α : Type u_1
E : Type ?u.42419
F : Type u_2
𝕜 : Type ?u.42425
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
h_two : ENNReal.ofReal 2 = 2
⊢ snorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
α : Type u_1
E : Type ?u.42419
F : Type u_2
𝕜 : Type ?u.42425
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
⊢ snorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
have h_two : ENNReal.ofReal (2 : ℝ) = 2 := by simp [zero_le_one]
α : Type u_1
E : Type ?u.42419
F : Type u_2
𝕜 : Type ?u.42425
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
h_two : ENNReal.ofReal 2 = 2
⊢ snorm (↑↑f) 2 μ ^ 2 < ⊤
α : Type u_1
E : Type ?u.42419
F : Type u_2
𝕜 : Type ?u.42425
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
h_two : ENNReal.ofReal 2 = 2
⊢ snorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
rw [snorm_norm_rpow f zero_lt_two, one_mul, h_two]
no goals
α : Type u_1
E : Type ?u.42419
F : Type u_2
𝕜 : Type ?u.42425
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
h_two : ENNReal.ofReal 2 = 2
⊢ snorm (↑↑f) 2 μ ^ 2 < ⊤
exact ENNReal.rpow_lt_top_of_nonneg zero_le_two (Lp.snorm_ne_top f)
no goals
α : Type u_1
E : Type ?u.42419
F : Type u_2
𝕜 : Type ?u.42425
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
⊢ ENNReal.ofReal 2 = 2
simp [zero_le_one]