α : Type u_3
E : Type ?u.107083
F : Type ?u.107086
F' : Type ?u.107089
G : Type ?u.107092
𝕜 : Type u_1
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' : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖(fun s => c • T s) s‖ ≤ ‖c‖ * C * ENNReal.toReal (↑↑μ s)
α : Type u_3
E : Type ?u.107083
F : Type ?u.107086
F' : Type ?u.107089
G : Type ?u.107092
𝕜 : Type u_1
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' : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
⊢ DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C)
refine' ⟨hT.1.smul c, fun s hs hμs => _⟩
α : Type u_3
E : Type ?u.107083
F : Type ?u.107086
F' : Type ?u.107089
G : Type ?u.107092
𝕜 : Type u_1
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' : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖c • T s‖ ≤ ‖c‖ * C * ENNReal.toReal (↑↑μ s)
α : Type u_3
E : Type ?u.107083
F : Type ?u.107086
F' : Type ?u.107089
G : Type ?u.107092
𝕜 : Type u_1
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' : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖(fun s => c • T s) s‖ ≤ ‖c‖ * C * ENNReal.toReal (↑↑μ s)
dsimp only
α : Type u_3
E : Type ?u.107083
F : Type ?u.107086
F' : Type ?u.107089
G : Type ?u.107092
𝕜 : Type u_1
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' : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖c‖ * ‖T s‖ ≤ ‖c‖ * (C * ENNReal.toReal (↑↑μ s))
α : Type u_3
E : Type ?u.107083
F : Type ?u.107086
F' : Type ?u.107089
G : Type ?u.107092
𝕜 : Type u_1
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' : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖c • T s‖ ≤ ‖c‖ * C * ENNReal.toReal (↑↑μ s)
rw [norm_smul, mul_assoc]
no goals
α : Type u_3
E : Type ?u.107083
F : Type ?u.107086
F' : Type ?u.107089
G : Type ?u.107092
𝕜 : Type u_1
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' : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖c‖ * ‖T s‖ ≤ ‖c‖ * (C * ENNReal.toReal (↑↑μ s))
exact mul_le_mul le_rfl (hT.2 s hs hμs) (norm_nonneg _) (norm_nonneg _)