α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.711091
G : Type ?u.711094
𝕜 : Type ?u.711097
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 α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤
    C * ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.711091
G : Type ?u.711094
𝕜 : Type ?u.711097
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 α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖setToL1S T f‖ ≤ C * ‖f‖
rw [setToL1S, norm_eq_sum_mul f]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.711091
G : Type ?u.711094
𝕜 : Type ?u.711097
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 α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ‖T s‖ ≤ C * ENNReal.toReal (↑↑μ s)
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤
    C * ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
exact
  SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable T hT_norm _
    (SimpleFunc.integrable f)