α : Type u_1
E : Type ?u.103681
F : Type ?u.103684
F' : Type ?u.103687
G : Type ?u.103690
𝕜 : Type ?u.103693
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' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖(T + T') s‖ ≤ (C + C') * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.103681
F : Type ?u.103684
F' : Type ?u.103687
G : Type ?u.103690
𝕜 : Type ?u.103693
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' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
⊢ DominatedFinMeasAdditive μ (T + T') (C + C')
refine' ⟨hT.1.add hT'.1, fun s hs hμs => _⟩
α : Type u_1
E : Type ?u.103681
F : Type ?u.103684
F' : Type ?u.103687
G : Type ?u.103690
𝕜 : Type ?u.103693
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' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖T s + T' s‖ ≤ C * ENNReal.toReal (↑↑μ s) + C' * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.103681
F : Type ?u.103684
F' : Type ?u.103687
G : Type ?u.103690
𝕜 : Type ?u.103693
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' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖(T + T') s‖ ≤ (C + C') * ENNReal.toReal (↑↑μ s)
rw [Pi.add_apply, add_mul]
no goals
α : Type u_1
E : Type ?u.103681
F : Type ?u.103684
F' : Type ?u.103687
G : Type ?u.103690
𝕜 : Type ?u.103693
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' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ‖T s + T' s‖ ≤ C * ENNReal.toReal (↑↑μ s) + C' * ENNReal.toReal (↑↑μ s)
exact (norm_add_le _ _).trans (add_le_add (hT.2 s hs hμs) (hT'.2 s hs hμs))