English
If f and g are functions into a normed space, the eLpNorm of the pointwise inner product is finite.
Русский
Для функций f,g в нормированном пространстве конечна eLpNorm от поэлементного скалярного произведения.
LaTeX
$$$ eLpNorm (\\lambda x. \\langle f(x), g(x)\\rangle) 1 \\mu < \\infty $$$
Lean4
theorem eLpNorm_inner_lt_top (f g : α →₂[μ] E) : eLpNorm (fun x : α => ⟪f x, g x⟫) 1 μ < ∞ :=
by
have h : ∀ x, ‖⟪f x, g x⟫‖ ≤ ‖‖f x‖ ^ (2 : ℝ) + ‖g x‖ ^ (2 : ℝ)‖ :=
by
intro x
rw [← @Nat.cast_two ℝ, Real.rpow_natCast, Real.rpow_natCast]
calc
‖⟪f x, g x⟫‖ ≤ ‖f x‖ * ‖g x‖ := norm_inner_le_norm _ _
_ ≤ 2 * ‖f x‖ * ‖g x‖ :=
(mul_le_mul_of_nonneg_right (le_mul_of_one_le_left (norm_nonneg _) one_le_two) (norm_nonneg _))
-- TODO(kmill): the type ascription is getting around an elaboration error
_ ≤ ‖(‖f x‖ ^ 2 + ‖g x‖ ^ 2 : ℝ)‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _)
refine (eLpNorm_mono_ae (ae_of_all _ h)).trans_lt ((eLpNorm_add_le ?_ ?_ le_rfl).trans_lt ?_)
· exact ((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable
· exact ((Lp.aestronglyMeasurable g).norm.aemeasurable.pow_const _).aestronglyMeasurable
rw [ENNReal.add_lt_top]
exact ⟨eLpNorm_rpow_two_norm_lt_top f, eLpNorm_rpow_two_norm_lt_top g⟩
