α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
b : E
hb : b ∈ SimpleFunc.range f
⊢ ‖T (↑f ⁻¹' {b})‖ * ‖b‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {b})) * ‖b‖
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, ‖T (↑f ⁻¹' {x})‖ * ‖x‖ ≤
    ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖
refine' Finset.sum_le_sum fun b hb => _
case inl
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
hb : 0 ∈ SimpleFunc.range f
⊢ ‖T (↑f ⁻¹' {0})‖ * ‖0‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {0})) * ‖0‖

case inr
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
b : E
hb✝ : b ∈ SimpleFunc.range f
hb : b ≠ 0
⊢ ‖T (↑f ⁻¹' {b})‖ * ‖b‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {b})) * ‖b‖
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
b : E
hb : b ∈ SimpleFunc.range f
⊢ ‖T (↑f ⁻¹' {b})‖ * ‖b‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {b})) * ‖b‖
obtain rfl | hb := eq_or_ne b 0
case inr.h
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
b : E
hb✝ : b ∈ SimpleFunc.range f
hb : b ≠ 0
⊢ ‖T (↑f ⁻¹' {b})‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {b}))
case inr
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
b : E
hb✝ : b ∈ SimpleFunc.range f
hb : b ≠ 0
⊢ ‖T (↑f ⁻¹' {b})‖ * ‖b‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {b})) * ‖b‖
gcongr
no goals
case inr.h
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
b : E
hb✝ : b ∈ SimpleFunc.range f
hb : b ≠ 0
⊢ ‖T (↑f ⁻¹' {b})‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {b}))
exact hT_norm _ (SimpleFunc.measurableSet_fiber _ _) <|
  SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hb
no goals
case inl
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
hb : 0 ∈ SimpleFunc.range f
⊢ ‖T (↑f ⁻¹' {0})‖ * ‖0‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {0})) * ‖0‖
simp
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖ ≤
    ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖ ≤
    C * ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖
simp_rw [mul_sum, ← mul_assoc]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.411774
F' : Type u_3
G : Type ?u.411780
𝕜 : Type ?u.411783
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 α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖ ≤
    ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖
rfl