The shift coupling of two weightings of a finite carrier

Two measures of equal finite total mass on a finite carrier that differ by a transfer of weight onto one designated atom k₀ -- so that ν' is dominated by ν everywhere else -- are coupled here by keeping the matched mass min (ν {k}) (ν' {k}) at (k, k) and putting the excess ν {k} - ν' {k} at (k, k₀). The mass this places off the diagonal is then at most the transferred weight, which is what a cost estimate against the diagonal consumes.

Mathlib has no maximal-coupling construction, and the general one is not needed here: dominance away from a single atom already says where the unmatched mass can go.

Main definitions

• TauCeti.MeasureTheory.shiftCoupling -- the coupling described above.

Main results

• TauCeti.MeasureTheory.shiftCoupling_apply -- its value on an arbitrary set;
• TauCeti.MeasureTheory.shiftCoupling_compl_diagonal_le_sum_tsub -- it puts at most the transferred mass off the diagonal;
• TauCeti.MeasureTheory.isCoupling_shiftCoupling -- it is a coupling of ν and ν'.

References

• TauCeti/Data/ENNReal/Weights.lean -- the arithmetic of the two weightings the marginals are computed from.

noncomputable def TauCeti.MeasureTheory.shiftCoupling {κ : Type u_1} [Fintype κ] [MeasurableSpace κ] (ν ν' : MeasureTheory.Measure κ) (k₀ : κ) : MeasureTheory.Measure (κ × κ)

The coupling of two weight vectors on a finite carrier that keeps as much mass as possible on the diagonal and transfers the excess of every other atom to the designated atom k₀.

It couples ν and ν' when their total singleton masses are equal and finite and ν' is dominated by ν away from k₀ (isCoupling_shiftCoupling), and the mass it puts off the diagonal is then bounded by the total transferred weight (shiftCoupling_compl_diagonal_le_sum_tsub).

Equations

• TauCeti.MeasureTheory.shiftCoupling ν ν' k₀ = ∑ k : κ, min (ν {k}) (ν' {k}) • MeasureTheory.Measure.dirac (k, k) + ∑ k : κ, (ν {k} - ν' {k}) • MeasureTheory.Measure.dirac (k, k₀)

theorem TauCeti.MeasureTheory.shiftCoupling_apply {κ : Type u_1} [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (ν ν' : MeasureTheory.Measure κ) (k₀ : κ) (S : Set (κ × κ)) : (shiftCoupling ν ν' k₀) S = ∑ k : κ, min (ν {k}) (ν' {k}) * S.indicator 1 (k, k) + ∑ k : κ, (ν {k} - ν' {k}) * S.indicator 1 (k, k₀)

The value of the shift coupling on an arbitrary set: the definition's body is not exposed, so this is the lemma downstream modules compute with.

theorem TauCeti.MeasureTheory.shiftCoupling_compl_diagonal_le_sum_tsub {κ : Type u_1} [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (ν ν' : MeasureTheory.Measure κ) (k₀ : κ) : (shiftCoupling ν ν' k₀) (Set.diagonal κ)ᶜ ≤ ∑ k : κ, (ν {k} - ν' {k})

The shift coupling puts at most the transferred mass off the diagonal. The matched mass sits on the diagonal by construction, and the excess of an atom k leaves the diagonal only when k ≠ k₀.

theorem TauCeti.MeasureTheory.isCoupling_shiftCoupling {κ : Type u_1} [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {ν ν' : MeasureTheory.Measure κ} {k₀ : κ} (hfg : ∑ k : κ, ν {k} = ∑ k : κ, ν' {k}) (hne : ∑ k : κ, ν {k} ≠ ⊤) (hdom : ∀ (k : κ), k ≠ k₀ → ν' {k} ≤ ν {k}) : IsCoupling ν ν' (shiftCoupling ν ν' k₀)

The shift coupling is a coupling. For measures with equal finite total singleton mass, its first marginal is ν because the matched mass and the excess add up at every atom, and its second marginal is ν' because the designated atom k₀ absorbs exactly the total excess.