CertificateAttainment.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.ShiftedCoulombCertificate.ofContactCandidate line 20

Source documentation

A contact candidate calibrates the common marginal potential integral. This constructs the abstract certificate without assuming the candidate is optimal.

def ofContactCandidate {mu : Measure E3} {pi0 : Measure Triple}
    (hpi0 : IsThreeCoupling mu pi0) {v : E3 → ℝ≥0∞} (hv : Measurable v)
    {offset : ℝ≥0∞} (hoffset : offset ≠ ⊤)
    (hbound : ∀ pi, IsThreeCoupling mu pi →
      ∀ᵐ t ∂pi, potentialSum v t ≤ coulombCost t + offset)
    (hcontact : ∀ᵐ t ∂pi0, potentialSum v t = coulombCost t + offset) :
    ShiftedCoulombCertificate mu (∫⁻ t, coulombCost t ∂pi0) where
…

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

theorem OAI.Problem356.candidateCost_lt_top_of_contact line 41

Source documentation

Finite marginal potential integral makes every contact candidate finite.

theorem candidateCost_lt_top_of_contact {mu : Measure E3} {pi0 : Measure Triple}
    (hpi0 : IsThreeCoupling mu pi0) {v : E3 → ℝ≥0∞} (hv : Measurable v)
    (hvfinite : (∫⁻ x, v x ∂mu) ≠ ⊤) {offset : ℝ≥0∞}
    (hcontact : ∀ᵐ t ∂pi0, potentialSum v t = coulombCost t + offset) :
    (∫⁻ t, coulombCost t ∂pi0) < ⊤ := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost

theorem OAI.Problem356.attained_finite_of_contact_candidate line 53
def OAI.Problem356.triplePotential line 72
Source documentation
The sum of the marginal potential over the three coordinates.
```
def triplePotential (p : E3 → ℝ≥0∞) (t : Triple) : ℝ≥0∞ :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple
theorem OAI.Problem356.measurable_triplePotential line 75
theorem OAI.Problem356.IsThreeCoupling.ae_of_support_certificate line 78
theorem OAI.Problem356.certificate_optimality line 94
theorem OAI.Problem356.kantorovichAttained_of_certificate line 105
theorem OAI.Problem356.certificate_contact_of_optimal line 115