α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
⊢ DominatedFinMeasAdditive μ T (ENNReal.toReal c * C)
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
⊢ DominatedFinMeasAdditive μ T (ENNReal.toReal c * C)
have h : ∀ s, MeasurableSet s → c • μ s = ∞ → μ s = ∞ := by
  intro s _ hcμs
  simp only [hc_ne_top, Algebra.id.smul_eq_mul, ENNReal.mul_eq_top, or_false_iff, Ne.def,
    false_and_iff] at hcμs
  exact hcμs.2
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖T s‖ ≤ ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
⊢ DominatedFinMeasAdditive μ T (ENNReal.toReal c * C)
refine' ⟨hT.1.of_eq_top_imp_eq_top (μ := c • μ) h, fun s hs hμs => _⟩
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hcμs : c • ↑↑μ s ≠ ⊤
⊢ ‖T s‖ ≤ ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖T s‖ ≤ ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
have hcμs : c • μ s ≠ ∞ := mt (h s hs) hμs.ne
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hcμs : c * ↑↑μ s ≠ ⊤
⊢ ‖T s‖ ≤ ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hcμs : c • ↑↑μ s ≠ ⊤
⊢ ‖T s‖ ≤ ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
rw [smul_eq_mul] at hcμs
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hcμs : c * ↑↑μ s ≠ ⊤
hT :
  FinMeasAdditive (c • μ) T ∧
    ∀ (s : Set α), MeasurableSet s → c * ↑↑μ s < ⊤ → ‖T s‖ ≤ C * (ENNReal.toReal c * ENNReal.toReal (↑↑μ s))
⊢ ‖T s‖ ≤ ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hcμs : c * ↑↑μ s ≠ ⊤
⊢ ‖T s‖ ≤ ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
simp_rw [DominatedFinMeasAdditive, Measure.smul_apply, smul_eq_mul, toReal_mul] at hT
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hcμs : c * ↑↑μ s ≠ ⊤
hT :
  FinMeasAdditive (c • μ) T ∧
    ∀ (s : Set α), MeasurableSet s → c * ↑↑μ s < ⊤ → ‖T s‖ ≤ C * (ENNReal.toReal c * ENNReal.toReal (↑↑μ s))
⊢ C * (ENNReal.toReal c * ENNReal.toReal (↑↑μ s)) = ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hcμs : c * ↑↑μ s ≠ ⊤
hT :
  FinMeasAdditive (c • μ) T ∧
    ∀ (s : Set α), MeasurableSet s → c * ↑↑μ s < ⊤ → ‖T s‖ ≤ C * (ENNReal.toReal c * ENNReal.toReal (↑↑μ s))
⊢ ‖T s‖ ≤ ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
refine' (hT.2 s hs hcμs.lt_top).trans (le_of_eq _)
no goals
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
h : ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hcμs : c * ↑↑μ s ≠ ⊤
hT :
  FinMeasAdditive (c • μ) T ∧
    ∀ (s : Set α), MeasurableSet s → c * ↑↑μ s < ⊤ → ‖T s‖ ≤ C * (ENNReal.toReal c * ENNReal.toReal (↑↑μ s))
⊢ C * (ENNReal.toReal c * ENNReal.toReal (↑↑μ s)) = ENNReal.toReal c * C * ENNReal.toReal (↑↑μ s)
ring
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
s : Set α
a✝ : MeasurableSet s
hcμs : c • ↑↑μ s = ⊤
⊢ ↑↑μ s = ⊤
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
⊢ ∀ (s : Set α), MeasurableSet s → c • ↑↑μ s = ⊤ → ↑↑μ s = ⊤
intro s _ hcμs
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
s : Set α
a✝ : MeasurableSet s
hcμs : ¬c = 0 ∧ ↑↑μ s = ⊤
⊢ ↑↑μ s = ⊤
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
s : Set α
a✝ : MeasurableSet s
hcμs : c • ↑↑μ s = ⊤
⊢ ↑↑μ s = ⊤
simp only [hc_ne_top, Algebra.id.smul_eq_mul, ENNReal.mul_eq_top, or_false_iff, Ne.def,
  false_and_iff] at hcμs
no goals
α : Type u_1
E : Type ?u.115680
F : Type ?u.115683
F' : Type ?u.115686
G : Type ?u.115689
𝕜 : Type ?u.115692
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive (c • μ) T C
s : Set α
a✝ : MeasurableSet s
hcμs : ¬c = 0 ∧ ↑↑μ s = ⊤
⊢ ↑↑μ s = ⊤
exact hcμs.2