The integral formula for the real L² norm #
The general-measure identity is shared by compactness and bilinear-form estimates.
theorem
EllipticPdes.Sobolev.norm_sq_L2_eq
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.Lp ℝ 2 μ))
:
The squared L² norm of any class is the integral of its square.