English
For f ∈ L2(μ; E), the L2-norm squared equals the real part of the integral of the squared pointwise norm via ENNReal-to-real conversion.
Русский
Для f ∈ L2(μ; E) квадрат нормы L2 равен вещественному преобразованию интеграла по μ от (‖f‖)^2.
LaTeX
$$$\\int_{α} ⟪f(a), f(a)⟫ \\, dμ(a) = \\mathrm{ENNReal.toReal}\\left( \\int_{α} (‖f(a)‖_+ )^2 \\, dμ(a) \\right)$$$
Lean4
theorem integral_inner_eq_sq_eLpNorm (f : α →₂[μ] E) :
∫ a, ⟪f a, f a⟫ ∂μ = ENNReal.toReal (∫⁻ a, (‖f a‖₊ : ℝ≥0∞) ^ (2 : ℝ) ∂μ) :=
by
simp_rw [inner_self_eq_norm_sq_to_K]
norm_cast
rw [integral_eq_lintegral_of_nonneg_ae]
rotate_left
· exact Filter.Eventually.of_forall fun x => sq_nonneg _
· exact ((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable
congr
ext1 x
have h_two : (2 : ℝ) = ((2 : ℕ) : ℝ) := by simp
rw [← Real.rpow_natCast _ 2, ← h_two, ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) zero_le_two,
ofReal_norm_eq_enorm]
norm_cast
