SeparatedLiftApproximation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.finiteMongeApproximation_of_near_fst_lifts line 15
Source documentation
Arbitrarily small first-coordinate lifts of a uniformly separated optimal coupling give finite Monge approximation. Only the first coordinate is adjusted to obtain a graph, and uniform separation controls the cost of that adjustment.
```
theorem finiteMongeApproximation_of_near_fst_lifts
    {mu : Measure E3} [IsProbabilityMeasure mu] {pi : Measure Triple}
    (hpi : IsThreeCoupling mu pi)
    (hoptimal : (∫⁻ t, coulombCost t ∂pi) = kantorovichValue mu)
    {eta : ℝ} (heta : 0 < eta)
    (hseparated : ∀ᵐ t ∂pi, CoulombEstimates.Separated eta t)
    (hlifts : ∀ delta : ℝ, 0 < delta →
      ∃ Q : E3 → Triple, Measurable Q ∧ Measure.map Q mu = pi ∧
        ∀ᵐ x ∂mu, dist x (Q x).1 ≤ delta) :
    FiniteMongeApproximation mu := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost, OAI.Problem356.kantorovichValue, OAI.Problem356.CoulombEstimates.Separated, OAI.Problem356.FiniteMongeApproximation

theorem OAI.Problem356.kantorovichValue_lt_top_of_separated_optimizer line 49

Source documentation

A uniformly separated optimal coupling has finite value.

theorem kantorovichValue_lt_top_of_separated_optimizer
    {mu : Measure E3} {pi : Measure Triple}
    (hpi : IsThreeCoupling mu pi)
    (hoptimal : (∫⁻ t, coulombCost t ∂pi) = kantorovichValue mu)
    {eta : ℝ} (heta : 0 < eta)
    (hseparated : ∀ᵐ t ∂pi, CoulombEstimates.Separated eta t) :
    kantorovichValue mu < ⊤ := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost, OAI.Problem356.kantorovichValue, OAI.Problem356.CoulombEstimates.Separated