DualCertificate.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.DualCertificate.potentialSum line 17
Source documentation
The sum of a nonnegative supporting potential over the three coordinates. A bounded signed potential can be shifted by a constant before using this sum.
```
def potentialSum (v : E3 → ℝ≥0∞) (t : Triple) : ℝ≥0∞ :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple
lemma OAI.Problem356.DualCertificate.measurable_potentialSum line 20
lemma OAI.Problem356.DualCertificate.lintegral_potentialSum line 27
Source documentation
The integral of a coordinate potential sum depends only on the common marginal.
```
lemma lintegral_potentialSum {mu : Measure E3} {pi : Measure Triple}
    (hpi : IsThreeCoupling mu pi) {v : E3 → ℝ≥0∞} (hv : Measurable v) :
    (∫⁻ t, potentialSum v t ∂pi) =
      (∫⁻ x, v x ∂mu) + (∫⁻ x, v x ∂mu) + (∫⁻ x, v x ∂mu) := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.DualCertificate.potentialSum

lemma OAI.Problem356.DualCertificate.lintegral_add_offset line 45

Source documentation

Adding a constant to a nonnegative cost shifts its integral by that constant under a probability measure; no measurability assumption on the cost is needed.

lemma lintegral_add_offset {α : Type uAlpha} [MeasurableSpace α]
    (pi : Measure α) [IsProbabilityMeasure pi] (c : α → ℝ≥0∞) (offset : ℝ≥0∞) :
    (∫⁻ t, c t + offset ∂pi) = (∫⁻ t, c t ∂pi) + offset := by
…

lemma OAI.Problem356.DualCertificate.ae_contact_of_equal_integrals line 52

Source documentation

Complementary slackness for a shifted nonnegative certificate.

lemma ae_contact_of_equal_integrals {α : Type uAlpha} [MeasurableSpace α]
    {pi : Measure α} [IsProbabilityMeasure pi] {p c : α → ℝ≥0∞}
    {offset : ℝ≥0∞} (hc : AEMeasurable c pi)
    (hbound : p ≤ᵐ[pi] fun t => c t + offset)
    (hfinite : (∫⁻ t, p t ∂pi) ≠ ⊤)
    (heq : (∫⁻ t, p t ∂pi) = (∫⁻ t, c t ∂pi) + offset) :
    p =ᵐ[pi] fun t => c t + offset := by
…

lemma OAI.Problem356.DualCertificate.ae_contact_of_optimal_coupling line 64

Source documentation

A finite shifted dual value forces every optimal coupling onto the contact set. The value identity is the sole input needed from dual optimality.

lemma ae_contact_of_optimal_coupling {mu : Measure E3} {pi : Measure Triple}
    (hpi : IsThreeCoupling mu pi) {v : E3 → ℝ≥0∞} (hv : Measurable v)
    {offset : ℝ≥0∞} (hoffset : offset ≠ ⊤)
    (hfinite : kantorovichValue mu ≠ ⊤)
    (hcost : AEMeasurable coulombCost pi)
    (hbound : potentialSum v ≤ᵐ[pi] fun t => coulombCost t + offset)
    (hvalue : (∫⁻ x, v x ∂mu) + (∫⁻ x, v x ∂mu) + (∫⁻ x, v x ∂mu) =
      kantorovichValue mu + offset)
    (hoptimal : (∫⁻ t, coulombCost t ∂pi) = kantorovichValue mu) :
    potentialSum v =ᵐ[pi] fun t => coulombCost t + offset := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.kantorovichValue, OAI.Problem356.coulombCost, OAI.Problem356.DualCertificate.potentialSum

lemma OAI.Problem356.DualCertificate.cost_strictly_above_of_noncontact line 84

Source documentation

If a feasible coupling is not concentrated on contact, its cost is strictly larger than a finite calibrated value. This is the contrapositive form needed for the deterministic-selection obstruction.

lemma cost_strictly_above_of_noncontact {mu : Measure E3} {pi : Measure Triple}
    (hpi : IsThreeCoupling mu pi) {v : E3 → ℝ≥0∞} (hv : Measurable v)
    {offset value : ℝ≥0∞} (hoffset : offset ≠ ⊤) (hfinite : value ≠ ⊤)
    (hcost : AEMeasurable coulombCost pi)
    (hbound : potentialSum v ≤ᵐ[pi] fun t => coulombCost t + offset)
    (hvalue : (∫⁻ x, v x ∂mu) + (∫⁻ x, v x ∂mu) + (∫⁻ x, v x ∂mu) =
      value + offset)
    (hnoncontact : ¬ (potentialSum v =ᵐ[pi] fun t => coulombCost t + offset)) :
    value < ∫⁻ t, coulombCost t ∂pi := by
…

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