eLpNorm_rpow_two_norm_lt_top — Mathlib

English

For f,g in Lp(μ) with values in E, the eLpNorm of ⟪f, g⟫ is finite.

Русский

Для f,g в Lp(μ) с значениями в E, конечна eLp-норма ⟪f,g⟫.

LaTeX

$$$ eLpNorm (\\lambda x. \\langle f(x), g(x)\\rangle) 1 \\mu < \\infty $$$

Lean4

theorem eLpNorm_rpow_two_norm_lt_top (f : Lp F 2 μ) : eLpNorm (fun x => ‖f x‖ ^ (2 : ℝ)) 1 μ < ∞ :=
  by
  have h_two : ENNReal.ofReal (2 : ℝ) = 2 := by simp
  rw [eLpNorm_norm_rpow f zero_lt_two, one_mul, h_two]
  exact ENNReal.rpow_lt_top_of_nonneg zero_le_two (Lp.eLpNorm_ne_top f)

Похожие утверждения