OptimalLocalization.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Problem356.ShiftedCoulombCertificate line 14
Source documentation
A nonnegative dual certificate after adding a finite constant to the cost. The shift permits a signed bounded real-valued supporting potential.
```
structure ShiftedCoulombCertificate (mu : Measure E3) (value : ℝ≥0∞) where
…
```
Mentions: OAI.Problem356.E3
theorem OAI.Problem356.ShiftedCoulombCertificate.measurable_coulomb line 27
theorem OAI.Problem356.ShiftedCoulombCertificate.lintegral_cost_add line 32
Source documentation
A constant shift integrates to itself under any feasible coupling.
```
theorem lintegral_cost_add (cert : ShiftedCoulombCertificate mu value)
    {pi : Measure Triple} (hpi : IsThreeCoupling mu pi) :
    (∫⁻ t, coulombCost t + cert.shift ∂pi) =
      (∫⁻ t, coulombCost t ∂pi) + cert.shift := by
…
```
Mentions: OAI.Problem356.ShiftedCoulombCertificate, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost
theorem OAI.Problem356.ShiftedCoulombCertificate.le_cost line 41
Source documentation
Every coupling has cost at least the certified value.
```
theorem le_cost (cert : ShiftedCoulombCertificate mu value)
    {pi : Measure Triple} (hpi : IsThreeCoupling mu pi) :
    value ≤ ∫⁻ t, coulombCost t ∂pi := by
…
```
Mentions: OAI.Problem356.ShiftedCoulombCertificate, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost
theorem OAI.Problem356.ShiftedCoulombCertificate.value_eq line 49
Source documentation
A feasible candidate matching a certificate realizes the exact infimum.
```
theorem value_eq (cert : ShiftedCoulombCertificate mu value)
    {pi : Measure Triple} (hpi : IsThreeCoupling mu pi)
    (hcost : (∫⁻ t, coulombCost t ∂pi) = value) :
    kantorovichValue mu = value := by
…
```
Mentions: OAI.Problem356.ShiftedCoulombCertificate, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost, OAI.Problem356.kantorovichValue
theorem OAI.Problem356.ShiftedCoulombCertificate.attained line 58
Source documentation
A matching candidate supplies the attainment assertion.
```
theorem attained (cert : ShiftedCoulombCertificate mu value)
    {pi : Measure Triple} (hpi : IsThreeCoupling mu pi)
    (hcost : (∫⁻ t, coulombCost t ∂pi) = value) :
    KantorovichAttained mu := by
…
```
Mentions: OAI.Problem356.ShiftedCoulombCertificate, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost, OAI.Problem356.KantorovichAttained
theorem OAI.Problem356.ShiftedCoulombCertificate.ae_contact line 66
Source documentation
Equality of the finite primal and dual integrals forces equality almost everywhere in the supporting inequality.
```
theorem ae_contact (cert : ShiftedCoulombCertificate mu value)
    (hfinite : value ≠ ⊤) {pi : Measure Triple}
    (hpi : IsThreeCoupling mu pi)
    (hcost : (∫⁻ t, coulombCost t ∂pi) = value) :
    ∀ᵐ t ∂pi, cert.potential t = coulombCost t + cert.shift := by
…
```
Mentions: OAI.Problem356.ShiftedCoulombCertificate, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost

theorem OAI.Problem356.ShiftedCoulombCertificate.ae_mem_of_optimal line 79

Source documentation

An optimal plan is concentrated on any prescribed set that contains the contact locus of the supporting certificate.

theorem ae_mem_of_optimal (cert : ShiftedCoulombCertificate mu value)
    (hfinite : value ≠ ⊤) (hvalue : kantorovichValue mu = value)
    {pi : Measure Triple} (hpi : IsThreeCoupling mu pi)
    (hopt : (∫⁻ t, coulombCost t ∂pi) = kantorovichValue mu)
    {contact : Set Triple}
    (hcontact : ∀ t, cert.potential t = coulombCost t + cert.shift → t ∈ contact) :
    ∀ᵐ t ∂pi, t ∈ contact := by
…

Mentions: OAI.Problem356.ShiftedCoulombCertificate, OAI.Problem356.kantorovichValue, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost

theorem OAI.Problem356.noMongeOptimizer_of_ne line 90