Pointwise products of L² functions on a product measure

For an L²(μ) function f and an L²(ν) function g on s-finite measures, the pointwise product (x, y) ↦ f x * g y belongs to L²(μ ⊗ ν), and the assignment factors the inner product as a tensor: ⟪f₁ ⊗ g₁, f₂ ⊗ g₂⟫ = ⟪f₁, f₂⟫ * ⟪g₁, g₂⟫. Consequently the products of two orthonormal families are an orthonormal family of L²(μ ⊗ ν).

For σ-finite factors the products of two Hilbert bases form a Hilbert basis HilbertBasis.prod of L²(μ ⊗ ν). Its index type is the product of the factor index types, and its basis vectors are the concrete pointwise products of the factor vectors.

The underlying normed-ring construction and its additive and scalar laws are provided by TauCeti.MeasureTheory.Function.Lp.Product.

The tensor family has dense linear span in L²(μ ⊗ ν) for arbitrary factor index types. Thus expansions in the product Hilbert basis are available without countability assumptions on either basis. The vanishing-integral lemmas relate orthogonality to all elementary tensors to the integrals of representatives over finite-measure rectangles and measurable sets.

The scalars are generic over [RCLike 𝕜], so a single construction serves both the real and complex L² spaces.

Main definitions

• MeasureTheory.Lp.prodMul — the pointwise product (x, y) ↦ f x * g y of F : L²(μ) and G : L²(ν) as a vector of L²(μ ⊗ ν).
• HilbertBasis.prod — the Hilbert basis of L²(μ ⊗ ν) built from Hilbert bases of the factors.

Main statements

• MeasureTheory.MemLp.mul_prod — the pointwise product of L² functions is L² for the product measure.
• MeasureTheory.Lp.inner_prodMul — the inner product of two tensors factors as a product of inner products.
• Orthonormal.prodMul — products of orthonormal families are orthonormal.
• HilbertBasis.orthogonal_span_range_prodMul_eq_bot — the basis tensors have trivial orthogonal complement.
• TauCeti.setIntegral_prod_eq_zero_of_forall_inner — orthogonality to every elementary tensor implies vanishing integrals over finite-measure rectangles.
• TauCeti.setIntegral_eq_zero_of_forall_inner — orthogonality to every elementary tensor implies vanishing integrals over all measurable sets of finite measure.
• HilbertBasis.prod_apply — the (i, j) basis vector is the tensor b₁ i ⊗ b₂ j; HilbertBasis.coeFn_prod gives its a.e. representative.

@[simp]

theorem MeasureTheory.Lp.inner_prodMul {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] (F₁ F₂ : ↥(Lp 𝕜 2 μ)) (G₁ G₂ : ↥(Lp 𝕜 2 ν)) : inner 𝕜 (prodMul F₁ G₁) (prodMul F₂ G₂) = inner 𝕜 F₁ F₂ * inner 𝕜 G₁ G₂

The tensor inner-product identity. The inner product of two pointwise-product vectors in L²(μ ⊗ ν) factors as the product of the inner products of the factors.

theorem Orthonormal.prodMul {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {ι₁ : Type u_4} {ι₂ : Type u_5} {b : ι₁ → ↥(MeasureTheory.Lp 𝕜 2 μ)} {c : ι₂ → ↥(MeasureTheory.Lp 𝕜 2 ν)} (hb : Orthonormal 𝕜 b) (hc : Orthonormal 𝕜 c) : Orthonormal 𝕜 fun (ij : ι₁ × ι₂) => MeasureTheory.Lp.prodMul (b ij.1) (c ij.2)

Orthonormality of the tensor family. If b and c are orthonormal families of L²(μ) and L²(ν), their pointwise products form an orthonormal family of L²(μ ⊗ ν), indexed by the product of index types.

@[simp]

theorem MeasureTheory.Lp.norm_prodMul {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] (F : ↥(Lp 𝕜 2 μ)) (G : ↥(Lp 𝕜 2 ν)) : ‖prodMul F G‖ = ‖F‖ * ‖G‖

The tensor construction is norm-multiplicative.

noncomputable def MeasureTheory.Lp.prodMulL {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] : ↥(Lp 𝕜 2 μ) →L[𝕜] ↥(Lp 𝕜 2 ν) →L[𝕜] ↥(Lp 𝕜 2 (μ.prod ν))

The tensor as a bounded bilinear map. prodMulL F G = prodMul F G, packaged so that either operand can be fixed: prodMulL F fixes the left factor, prodMulL.flip G the right. Its operator norm is at most 1.

Equations

• MeasureTheory.Lp.prodMulL = (LinearMap.mk₂ 𝕜 MeasureTheory.Lp.prodMul ⋯ ⋯ ⋯ ⋯).mkContinuous₂ 1 ⋯

@[simp]

theorem MeasureTheory.Lp.prodMulL_apply {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] (F : ↥(Lp 𝕜 2 μ)) (G : ↥(Lp 𝕜 2 ν)) : (prodMulL F) G = prodMul F G

theorem HilbertBasis.inner_prodMul_eq_zero_of_forall_basis {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {ι₁ : Type u_4} {ι₂ : Type u_5} (b₁ : HilbertBasis ι₁ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 μ)) (b₂ : HilbertBasis ι₂ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 ν)) {h : ↥(MeasureTheory.Lp 𝕜 2 (μ.prod ν))} (hz : ∀ (i : ι₁) (j : ι₂), inner 𝕜 h (MeasureTheory.Lp.prodMul (b₁ i) (b₂ j)) = 0) (F : ↥(MeasureTheory.Lp 𝕜 2 μ)) (G : ↥(MeasureTheory.Lp 𝕜 2 ν)) : inner 𝕜 h (MeasureTheory.Lp.prodMul F G) = 0

Basis tensors detect all tensors. A vector orthogonal to every tensor built from two Hilbert bases is orthogonal to every elementary tensor. Thus the basis tensors suffice for testing orthogonality to the family of elementary tensors.

theorem TauCeti.setIntegral_prod_eq_zero_of_forall_inner {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {h : ↥(MeasureTheory.Lp 𝕜 2 (μ.prod ν))} (hz : ∀ (F : ↥(MeasureTheory.Lp 𝕜 2 μ)) (G : ↥(MeasureTheory.Lp 𝕜 2 ν)), inner 𝕜 (MeasureTheory.Lp.prodMul F G) h = 0) {A : Set α} (hA : MeasurableSet A) (hμA : μ A ≠ ⊤) {B : Set β} (hB : MeasurableSet B) (hνB : ν B ≠ ⊤) : ∫ (p : α × β) in A ×ˢ B, ↑↑h p ∂μ.prod ν = 0

A vector orthogonal to every elementary tensor has vanishing integral over every measurable rectangle whose sides have finite measure. This determines its averages on such rectangles.

theorem TauCeti.setIntegral_eq_zero_of_forall_inner {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] {h : ↥(MeasureTheory.Lp 𝕜 2 (μ.prod ν))} (hz : ∀ (F : ↥(MeasureTheory.Lp 𝕜 2 μ)) (G : ↥(MeasureTheory.Lp 𝕜 2 ν)), inner 𝕜 (MeasureTheory.Lp.prodMul F G) h = 0) (u : Set (α × β)) (hu : MeasurableSet u) (hfin : (μ.prod ν) u < ⊤) : ∫ (p : α × β) in u, ↑↑h p ∂μ.prod ν = 0

A vector orthogonal to every elementary tensor has vanishing integral over every measurable set of finite measure.

theorem HilbertBasis.orthogonal_span_range_prodMul_eq_bot {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] {ι₁ : Type u_4} {ι₂ : Type u_5} (b₁ : HilbertBasis ι₁ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 μ)) (b₂ : HilbertBasis ι₂ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 ν)) : (Submodule.span 𝕜 (Set.range fun (ij : ι₁ × ι₂) => MeasureTheory.Lp.prodMul (b₁ ij.1) (b₂ ij.2)))ᗮ = ⊥

Completeness of the tensor family. The tensors built from two Hilbert bases have trivial orthogonal complement in L²(μ ⊗ ν). Together with orthonormality, this supplies the completeness condition for the product Hilbert basis.

noncomputable def HilbertBasis.prod {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] {ι₁ : Type u_4} {ι₂ : Type u_5} (b₁ : HilbertBasis ι₁ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 μ)) (b₂ : HilbertBasis ι₂ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 ν)) : HilbertBasis (ι₁ × ι₂) 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (μ.prod ν))

The product Hilbert basis. Pointwise products of two Hilbert bases form a Hilbert basis of L²(μ ⊗ ν), indexed by the product of the index types.

Equations

• b₁.prod b₂ = HilbertBasis.mkOfOrthogonalEqBot ⋯ ⋯

@[simp]

theorem HilbertBasis.prod_apply {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] {ι₁ : Type u_4} {ι₂ : Type u_5} (b₁ : HilbertBasis ι₁ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 μ)) (b₂ : HilbertBasis ι₂ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 ν)) (ij : ι₁ × ι₂) : (b₁.prod b₂) ij = MeasureTheory.Lp.prodMul (b₁ ij.1) (b₂ ij.2)

The vector of HilbertBasis.prod at ij is the tensor of the corresponding factor vectors.

theorem HilbertBasis.coeFn_prod {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] {ι₁ : Type u_4} {ι₂ : Type u_5} (b₁ : HilbertBasis ι₁ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 μ)) (b₂ : HilbertBasis ι₂ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 ν)) (ij : ι₁ × ι₂) : ↑↑((b₁.prod b₂) ij) =ᵐ[μ.prod ν] fun (q : α × β) => ↑↑(b₁ ij.1) q.1 * ↑↑(b₂ ij.2) q.2

The vector of HilbertBasis.prod at ij is a.e. the pointwise product of its factors.