Inner products of square-integrable functions #
The pointwise inner product of two square-integrable functions with values in an inner product
space is integrable. Mathlib states this for elements of L² (MeasureTheory.L2.integrable_inner);
this file gives the form for functions satisfying MemLp f 2 μ, which is how second-moment
hypotheses on random vectors are usually stated, together with the special case of a quadratic
form ⟪B (f x), f x⟫ of a matrix B on a Euclidean-valued function.
For counting measure, singleton-supported vectors separate L² functions and determine
continuous linear maps out of L². On a compact space with a finite measure, the L² pairing of an
L² function with a continuous function is an integral
(MeasureTheory.L2.inner_toLp_continuousMap), extending Mathlib's ContinuousMap.inner_toLp.
More generally, the L² pairing of an L² function with the class of any square-integrable
function is the integral of their pointwise inner product (MeasureTheory.L2.inner_toLp).
The integral of ⟪f x, c⟫ is ⟪∫ f, c⟫ (integral_inner_left), the counterpart of Mathlib's
integral_inner with the integrand in the left slot.
Indicators of any countably spanning generating π-system of finite-measure sets have
dense real linear span in L².
The space L²(μ) is infinite-dimensional as soon as μ carries infinitely many pairwise disjoint
sets of positive finite measure (MeasureTheory.L2.not_finiteDimensional_of_pairwise_disjoint),
since their indicators are nonzero and pairwise orthogonal. In particular L² of an open-positive,
locally finite measure restricted to a nonempty open subset of a nontrivial real normed space is
infinite-dimensional (MeasureTheory.L2.not_finiteDimensional_restrict_of_isOpen), which applies
to Lebesgue measure on a nonempty open subset of ℝⁿ, n ≥ 1.
For a complex inner product space F regarded as a real one (InnerProductSpace.complexToReal),
the real inner product on L²(α, F) is the real part of the complex one
(MeasureTheory.L2.real_inner_eq_re_inner). For a family of inner product spaces G i, evaluating
coordinate i of an L²(α, ℓ²(G)) function is adjoint to placing an L²(α, G i) function in
coordinate i (MeasureTheory.L2.inner_evalCLM_compLpL).
The pointwise inner product of two square-integrable functions is integrable.
The quadratic form of a matrix on a square-integrable Euclidean-valued function is integrable.
A counting-measure L² function orthogonal to every singleton-supported vector is zero. No countability of the underlying measurable space is needed.
On a compact space with a finite measure, the L² inner product of an L² function f with a
continuous function g is the integral of their pointwise inner product.
L² is infinite-dimensional when the measure carries a sequence of pairwise disjoint
measurable sets of positive finite measure: their indicators are nonzero and pairwise
orthogonal, hence linearly independent.
L² of a nonempty open set is infinite-dimensional. For an open-positive, locally finite
measure on a nontrivial real normed space, L² of its restriction to a nonempty open set U is
not finite-dimensional. The witnesses are indicators of disjoint concentric annuli in a small
ball inside U.
For a complex inner product space F with its induced real structure, the real inner product
on L²(α, F) is the real part of the complex one.
Evaluating coordinate i of an L²(α, ℓ²(G)) function is adjoint to placing an
L²(α, G i) function in coordinate i.
The L² inner product of an L² function f with the class of a square-integrable function
g is the integral of their pointwise inner product.
A continuous linear map out of counting-measure L² that vanishes on all singleton-supported vectors is zero. No countability of the index space is needed.
Integration commutes with the inner product against a fixed vector in the right slot:
∫ ⟪f x, c⟫ = ⟪∫ f, c⟫. This is integral_inner with the integrand in the left slot.
Indicators of a countably spanning generating π-system of finite-measure sets have dense real linear span in L².