α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type ?u.197555
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.197657
F' : Type ?u.197660
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
⊢ C * ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖ =
    C * ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • ‖x‖
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type ?u.197555
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.197657
F' : Type ?u.197660
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
⊢ C * ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖ = C * integral μ (map norm f)
rw [map_integral f norm hf norm_zero]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type ?u.197555
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.197657
F' : Type ?u.197660
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : α →ₛ E
hf : Integrable ↑f
⊢ C * ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) * ‖x‖ =
    C * ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • ‖x‖
simp_rw [smul_eq_mul]