Limits of coupling densities in L¹

For finite marginals, the coupling constraint is closed under L¹ convergence of densities against a σ-finite reference measure. An integrable, almost everywhere nonnegative limit defines a coupling of the same marginals. No topology on the underlying measurable spaces is required, and the reference measure may have infinite mass.

TauCeti.isCoupling_withDensity_of_tendsto_eLpNorm applies along any nontrivial filter. It is the measure-theoretic closure step used when constructing a transport plan from a convergent family of densities, independently of the functional that is being minimized.

theorem TauCeti.isCoupling_withDensity_of_tendsto_eLpNorm {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {R : MeasureTheory.Measure (X × Y)} {l : Filter ι} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite R] [l.NeBot] {π : ι → MeasureTheory.Measure (X × Y)} (hπ : ∀ (i : ι), IsCoupling (π i) μ ν) (hac : ∀ (i : ι), (π i).AbsolutelyContinuous R) {g : X × Y → ℝ} (hgint : MeasureTheory.Integrable g R) (hg0 : 0 ≤ᵐ[R] g) (hL1 : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm ((fun (z : X × Y) => ((π i).rnDeriv R z).toReal) - g) 1 R) l (nhds 0)) : IsCoupling (R.withDensity fun (z : X × Y) => ENNReal.ofReal (g z)) μ ν

If the densities of couplings of μ and ν against a σ-finite reference R converge in L¹(R) along a nontrivial filter to an integrable, almost everywhere nonnegative function, that function is the density of a coupling of μ and ν. The source measure μ is finite.