CompactLiftApproximation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.finiteMongeApproximation_of_compact_separated_optimizer line 15

Source documentation

A compactly supported atomless marginal and a uniformly separated optimal coupling admit finite-cost deterministic approximations.

theorem finiteMongeApproximation_of_compact_separated_optimizer
    {mu : Measure E3} [IsProbabilityMeasure mu] [NullSingletonClass mu]
    {pi : Measure Triple} (hpi : IsThreeCoupling mu pi)
    (hoptimal : (∫⁻ t, coulombCost t ∂pi) = kantorovichValue mu)
    {K : Set E3} (hK : IsCompact K) (hfull : mu Kᶜ = 0)
    {eta : ℝ} (heta : 0 < eta)
    (hseparated : ∀ᵐ t ∂pi, CoulombEstimates.Separated eta t) :
    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.HasCoulombCounterexample.hasFull_of_separated_optimizer line 32
Source documentation
A Coulomb counterexample with a separated optimal plan and compactly supported density has equal Monge and Kantorovich infima and finite-cost Monge approximations.
```
theorem HasCoulombCounterexample.hasFull_of_separated_optimizer
    {rho : E3 → ℝ} (hcounter : HasCoulombCounterexample rho)
    {pi : Measure Triple} (hpi : IsThreeCoupling (densityMeasure rho) pi)
    (hoptimal : (∫⁻ t, coulombCost t ∂pi) = kantorovichValue (densityMeasure rho))
    {eta : ℝ} (heta : 0 < eta)
    (hseparated : ∀ᵐ t ∂pi, CoulombEstimates.Separated eta t) :
    HasFullCoulombConclusion rho := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.HasCoulombCounterexample, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.densityMeasure, OAI.Problem356.coulombCost, OAI.Problem356.kantorovichValue, OAI.Problem356.CoulombEstimates.Separated, OAI.Problem356.HasFullCoulombConclusion