EqualInfima.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.mongeValue_le_graphCost line 12
Source documentation
Every feasible Monge pair bounds its defining infimum from above.
```
theorem mongeValue_le_graphCost (mu : Measure E3) {T2 T3 : E3 → E3}
    (h2 : Preserves mu T2) (h3 : Preserves mu T3) :
    mongeValue mu ≤ graphCost mu T2 T3 := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Preserves, OAI.Problem356.mongeValue, OAI.Problem356.graphCost
theorem OAI.Problem356.FiniteMongeApproximation.equal_infima line 18
Source documentation
Arbitrarily accurate finite preserving-map approximations imply equality of values.
```
theorem FiniteMongeApproximation.equal_infima {mu : Measure E3}
    [IsProbabilityMeasure mu] (h : FiniteMongeApproximation mu) :
    mongeValue mu = kantorovichValue mu := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.FiniteMongeApproximation, OAI.Problem356.mongeValue, OAI.Problem356.kantorovichValue
theorem OAI.Problem356.finiteMongeApproximation_of_equal_infima line 28
Source documentation
Finite equality of values already supplies finite near-minimizing preserving maps.
```
theorem finiteMongeApproximation_of_equal_infima {mu : Measure E3}
    (hfinite : kantorovichValue mu < ⊤)
    (heq : mongeValue mu = kantorovichValue mu) :
    FiniteMongeApproximation mu := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.kantorovichValue, OAI.Problem356.mongeValue, OAI.Problem356.FiniteMongeApproximation
theorem OAI.Problem356.finiteMongeApproximation_iff_equal_infima line 44
Source documentation
Under finiteness, equal infima and finite Monge approximation are equivalent.
```
theorem finiteMongeApproximation_iff_equal_infima {mu : Measure E3}
    [IsProbabilityMeasure mu] (hfinite : kantorovichValue mu < ⊤) :
    FiniteMongeApproximation mu ↔ mongeValue mu = kantorovichValue mu :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.kantorovichValue, OAI.Problem356.FiniteMongeApproximation, OAI.Problem356.mongeValue
theorem OAI.Problem356.HasCoulombCounterexample.fullConclusion line 51
Source documentation
The full target conclusion follows once the counterexample and finite approximation have been constructed for the same density.
```
theorem HasCoulombCounterexample.fullConclusion {rho : E3 → ℝ}
    (h : 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