Endgame.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.mongeValue_eq_kantorovichValue_of_finiteMongeApproximation line 14
Source documentation
Finite graph approximants give the reverse relaxation inequality, hence identify the Monge and Kantorovich infima.
```
theorem mongeValue_eq_kantorovichValue_of_finiteMongeApproximation
    (mu : Measure E3) [IsProbabilityMeasure mu] (happrox : FiniteMongeApproximation mu) :
    mongeValue mu = kantorovichValue mu := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.FiniteMongeApproximation, OAI.Problem356.mongeValue, OAI.Problem356.kantorovichValue
theorem OAI.Problem356.hasFullCoulombConclusion_of_counterexample_of_approximation line 31
Source documentation
The final logical closure: counterexample construction plus finite Monge approximation gives the complete qualified conclusion without changing any of its predicates.
```
theorem hasFullCoulombConclusion_of_counterexample_of_approximation
    {rho : E3 → ℝ} (hcounter : HasCoulombCounterexample rho)
    (happrox : FiniteMongeApproximation (densityMeasure rho)) :
    HasFullCoulombConclusion rho := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.HasCoulombCounterexample, OAI.Problem356.FiniteMongeApproximation, OAI.Problem356.densityMeasure, OAI.Problem356.HasFullCoulombConclusion