α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ ‖f‖ ^ 2 = ↑IsROrC.re (inner f f)
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ‖f‖ ^ 2 = ↑IsROrC.re (inner f f)
have h_two : (2 : ℝ≥0∞).toReal = 2 := by simp
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm (↑↑f) 2 μ ^ 2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ

α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ) ≠ ⊤
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ ‖f‖ ^ 2 = ↑IsROrC.re (inner f f)
rw [inner_def, integral_inner_eq_sq_snorm, norm_def, ← ENNReal.toReal_pow, IsROrC.ofReal_re,
  ENNReal.toReal_eq_toReal (ENNReal.pow_ne_top (Lp.snorm_ne_top f)) _]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ENNReal.toReal 2 = 2
simp
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ) ^ (2⁻¹ * ↑2) = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm (↑↑f) 2 μ ^ 2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
rw [← ENNReal.rpow_nat_cast, snorm_eq_snorm' two_ne_zero ENNReal.two_ne_top, snorm', ←
  ENNReal.rpow_mul, one_div, h_two]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ) ^ (2⁻¹ * ↑2) = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
simp
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm' (fun a => ↑↑f a) 2 μ < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ) ≠ ⊤
refine' (lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top zero_lt_two _).ne
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm (fun a => ↑↑f a) 2 μ < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm' (fun a => ↑↑f a) 2 μ < ⊤
rw [← h_two, ← snorm_eq_snorm' two_ne_zero ENNReal.two_ne_top]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.54916
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm (fun a => ↑↑f a) 2 μ < ⊤
exact Lp.snorm_lt_top f