CouplingSupport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem356.IsThreeCoupling.ae_coordinates line 15
Source documentation
A property holding almost everywhere for the common marginal holds in all three coordinates of every feasible coupling. No measurability of the property is needed for this direction of transport.
```
lemma IsThreeCoupling.ae_coordinates {mu : Measure E3} {pi : Measure Triple}
    (hpi : IsThreeCoupling mu pi) {p : E3 → Prop} (hp : ∀ᵐ x ∂mu, p x) :
    ∀ᵐ t ∂pi, p (tripleFst t) ∧ p (tripleSnd t) ∧ p (tripleThd t) := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.tripleFst, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd

lemma OAI.Problem356.ae_mem_of_probability_measure_eq_one line 30

Source documentation

Full marginal mass on a measurable set gives almost-everywhere membership.

lemma ae_mem_of_probability_measure_eq_one {mu : Measure E3} [IsProbabilityMeasure mu]
    {U : Set E3} (hU : MeasurableSet U) (hfull : mu U = 1) :
    ∀ᵐ x ∂mu, x ∈ U := by
…

Mentions: OAI.Problem356.E3

lemma OAI.Problem356.IsThreeCoupling.ae_mem_cube line 38
Source documentation
Every coupling of a probability carried by U is carried by U³.
```
lemma IsThreeCoupling.ae_mem_cube {mu : Measure E3} [IsProbabilityMeasure mu]
    {pi : Measure Triple} (hpi : IsThreeCoupling mu pi)
    {U : Set E3} (hU : MeasurableSet U) (hfull : mu U = 1) :
    ∀ᵐ t ∂pi, tripleFst t ∈ U ∧ tripleSnd t ∈ U ∧ tripleThd t ∈ U :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.tripleFst, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd

lemma OAI.Problem356.IsThreeCoupling.ae_of_on_cube line 46

Source documentation

A pointwise certificate on the full-mass cube may be used almost everywhere against any feasible coupling.

lemma IsThreeCoupling.ae_of_on_cube {mu : Measure E3} [IsProbabilityMeasure mu]
    {pi : Measure Triple} (hpi : IsThreeCoupling mu pi)
    {U : Set E3} (hU : MeasurableSet U) (hfull : mu U = 1)
    {P : Triple → Prop}
    (hP : ∀ t, tripleFst t ∈ U → tripleSnd t ∈ U → tripleThd t ∈ U → P t) :
    ∀ᵐ t ∂pi, P t := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.tripleFst, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd