case h.h
α : Type u_1
E : Type ?u.398702
F : Type u_2
F' : Type u_3
G : Type ?u.398711
𝕜 : Type ?u.398714
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 α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ F
i✝ : F
a✝ : i✝ ∈ SimpleFunc.range f
⊢ ‖T (↑f ⁻¹' {i✝})‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {i✝}))
α : Type u_1
E : Type ?u.398702
F : Type u_2
F' : Type u_3
G : Type ?u.398711
𝕜 : Type ?u.398714
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 α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ F
⊢ ∑ x in SimpleFunc.range f, ‖T (↑f ⁻¹' {x})‖ * ‖x‖ ≤
    ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖
gcongr
no goals
case h.h
α : Type u_1
E : Type ?u.398702
F : Type u_2
F' : Type u_3
G : Type ?u.398711
𝕜 : Type ?u.398714
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 α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ F
i✝ : F
a✝ : i✝ ∈ SimpleFunc.range f
⊢ ‖T (↑f ⁻¹' {i✝})‖ ≤ C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {i✝}))
exact hT_norm _ <| SimpleFunc.measurableSet_fiber _ _
α : Type u_1
E : Type ?u.398702
F : Type u_2
F' : Type u_3
G : Type ?u.398711
𝕜 : Type ?u.398714
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 α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ 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.398702
F : Type u_2
F' : Type u_3
G : Type ?u.398711
𝕜 : Type ?u.398714
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 α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ 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.398702
F : Type u_2
F' : Type u_3
G : Type ?u.398711
𝕜 : Type ?u.398714
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 α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ F
⊢ ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖ ≤
    ∑ x in SimpleFunc.range f, C * ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖
rfl