Existence and uniqueness of the outer L² class #
Uniqueness of an outer L² class from its nested a.e. representative formula.
A strongly measurable product L² function has a uniquely characterized outer L² class. The target separability is used only to establish measurability.
theorem
LiebThirring.l2_curry_unique
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
(f : α × β → E)
(c d : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp E 2 ν)) 2 μ))
(hc : ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, ↑↑(↑↑c x) y = f (x, y))
(hd : ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, ↑↑(↑↑d x) y = f (x, y))
:
Uniqueness of an outer L² class from its nested a.e. representative formula.
theorem
LiebThirring.existsUnique_l2_curry
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[SecondCountableTopology ↥(MeasureTheory.Lp E 2 ν)]
(f : α × β → E)
(hf : MeasureTheory.StronglyMeasurable f)
(hLp : MeasureTheory.MemLp f 2 (μ.prod ν))
:
A strongly measurable product L² function has a uniquely characterized outer L² class. The target separability is used only to establish measurability.