Pointwise products of square-integrable functions on a product measure

The product (x, y) ↦ f x * g y of two square-integrable functions with values in a nonunital normed ring is square-integrable for the product measure. Only the second measure needs to be s-finite. MeasureTheory.MemLp.mul_prod gives membership, while MeasureTheory.Lp.prodMul packages the product as an Lp vector with its almost-everywhere representative and additive and scalar laws.

The norm need only be submultiplicative. A normed ring supplies its own left scalar action, and homogeneity in the second argument with respect to that action requires commutativity.

theorem MeasureTheory.MemLp.mul_prod {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite ν] [NonUnitalNormedRing 𝕜] {f : α → 𝕜} {g : β → 𝕜} (hf : MemLp f 2 μ) (hg : MemLp g 2 ν) : MemLp (fun (p : α × β) => f p.1 * g p.2) 2 (μ.prod ν)

The pointwise product (x, y) ↦ f x * g y of an L²(μ) and an L²(ν) function is L² for the product measure μ ⊗ ν.

noncomputable def MeasureTheory.Lp.prodMul {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite ν] [NonUnitalNormedRing 𝕜] (F : ↥(Lp 𝕜 2 μ)) (G : ↥(Lp 𝕜 2 ν)) : ↥(Lp 𝕜 2 (μ.prod ν))

The pointwise product (x, y) ↦ F x * G y of F : L²(μ) and G : L²(ν), as a vector of L²(μ ⊗ ν).

Equations

• MeasureTheory.Lp.prodMul F G = MeasureTheory.MemLp.toLp (fun (p : α × β) => ↑↑F p.1 * ↑↑G p.2) ⋯

theorem MeasureTheory.Lp.coeFn_prodMul {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {ν : Measure β} [SFinite ν] [NonUnitalNormedRing 𝕜] (F : ↥(Lp 𝕜 2 μ)) (G : ↥(Lp 𝕜 2 ν)) : ↑↑(prodMul F G) =ᵐ[μ.prod ν] fun (p : α × β) => ↑↑F p.1 * ↑↑G p.2

The Lp representative of prodMul F G is the pointwise product of the representatives.

@[simp]

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

The tensor is additive in its first argument.

@[simp]

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

The tensor is additive in its second argument.

@[simp]

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

The tensor vanishes when its first argument does.

@[simp]

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

The tensor vanishes when its second argument does.

@[simp]

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

The tensor is homogeneous in its first argument.

@[simp]

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

The tensor is homogeneous in its second argument.