Pointwise products of L² functions on a finite product measure #
For a finite family of σ-finite measures μ i and L²(μ i) functions f i, the pointwise product
x ↦ ∏ i, f i (x i) belongs to L²(Measure.pi μ), the assignment factors the inner product as a
tensor, and coordinatewise Hilbert bases multiply to a Hilbert basis TauCeti.piHilbertBasis of
L²(Measure.pi μ). This is the Fintype-indexed analogue of the binary product basis
HilbertBasis.prod.
Main definitions #
TauCeti.L2piMul— the pointwise productx ↦ ∏ i, F i (x i)as a vector ofL²(Measure.pi μ).TauCeti.piHilbertBasis— the Hilbert basis ofL²(Measure.pi μ)built from coordinatewise Hilbert bases.
Main statements #
TauCeti.memLp_pi_prod— the pointwise product ofL²functions isL²for the product measure.TauCeti.integrable_L2piMul_mul— a product ofL²factors times anL²function is integrable.TauCeti.inner_L2piMul— the inner product of two tensors factors coordinatewise.TauCeti.orthonormal_L2piMul— coordinatewise orthonormal families multiply to an orthonormal family.TauCeti.orthogonal_span_range_L2piMul_eq_bot— the basis tensors have trivial orthogonal complement.TauCeti.piHilbertBasis_apply,TauCeti.coeFn_piHilbertBasis— thek-th basis vector is the tensor of thek i-th coordinate basis vectors, a.e. equal to∏ i, b i (k i).TauCeti.piHilbertBasis_repr_L2piMul— the coordinates of a tensor are the products of its coordinatewise coordinates.
Implementation notes #
Orthonormality follows from Mathlib's Fubini theorem integral_fintype_prod_eq_prod.
Completeness assumes no countability of the index types κ i and runs in three steps:
TauCeti.inner_L2piMul_eq_zero_of_forall_basis— orthogonality to the basis tensors upgrades to orthogonality to every elementary tensor, byFinsetinduction on the coordinates, pushing a basis expansion of one slot through the continuous linear mapTauCeti.L2piMulSlot.TauCeti.setIntegral_pi_eq_zero_of_forall_inner— testing against indicators, since a tensor of indicators is the indicator of the box.TauCeti.setIntegral_eq_zero_of_forall_inner_pi— the Dynkin (π-λ) stepTauCeti.setIntegral_eq_zero_of_isPiSystemapplied toisPiSystem_piinside a finite box, followed by a monotone exhaustion along∏ i, spanningSets (μ i) n.
The pointwise product x ↦ ∏ i, f i (x i) of L² functions is L² for the product measure.
The pointwise product x ↦ ∏ i, F i (x i) of a family of L²(μ i) vectors, as a vector of
L²(Measure.pi μ).
Equations
- TauCeti.L2piMul F = MeasureTheory.MemLp.toLp (fun (x : (i : ι) → α i) => ∏ i : ι, ↑↑(F i) (x i)) ⋯
Instances For
The Lp representative of L2piMul F is the pointwise product of the representatives.
A pointwise product of coordinatewise L² functions times an L² function on the product
space is integrable.
Splitting off the j-th coordinate of a tensor.
The tensor is additive in the j-th coordinate.
The tensor is homogeneous in the j-th coordinate.
The tensor vanishes when its j-th coordinate does.
The tensor inner-product identity, Fintype-indexed. The inner product of two pointwise
products factors as the product of the coordinatewise inner products.
Orthonormality of the tensor family, Fintype-indexed. Coordinatewise orthonormal families
multiply to an orthonormal family of L²(Measure.pi μ), indexed by the dependent function type.
The tensor construction is norm-multiplicative.
The norm of a tensor with its j-th coordinate replaced.
Tensoring with all coordinates but j held fixed, as a continuous linear map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
L2piMulSlot applies as the tensor.
Basis tensors detect all tensors. A vector orthogonal to every tensor built from coordinatewise Hilbert bases is orthogonal to every elementary tensor.
A vector orthogonal to every elementary tensor has vanishing integral over every box whose sides are measurable sets of finite measure.
A vector orthogonal to every elementary tensor has vanishing integral over every measurable set of finite measure.
Completeness of the tensor family. The tensors built from coordinatewise Hilbert bases have
trivial orthogonal complement in L²(Measure.pi μ).
The Fintype-indexed product Hilbert basis. Pointwise products of coordinatewise Hilbert
bases form a Hilbert basis of L²(Measure.pi μ), indexed by the dependent function type.
Equations
Instances For
The k-th vector of piHilbertBasis is the tensor of the k i-th basis vectors.
The coordinate of a tensor in a product Hilbert basis is the product of its coordinatewise coordinates.
The k-th vector of piHilbertBasis is a.e. the pointwise product ∏ i, b i (k i).