α : Type u_1
E : Type u_2
F : Type ?u.97006
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
⊢ snorm (fun x => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.97006
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
⊢ AEEqFun.mk (fun x => inner (↑↑f x) (↑↑g x)) (_ : AEStronglyMeasurable (fun x => inner (↑↑f x) (↑↑g x)) μ) ∈ Lp 𝕜 1
simp_rw [mem_Lp_iff_snorm_lt_top, snorm_aeeqFun]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.97006
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
⊢ snorm (fun x => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤
exact snorm_inner_lt_top f g