CertificateDuality.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.Certificate.ofReal_integral_le_lintegral line 14

Source documentation

An integrable signed lower certificate bounds a nonnegative extended integral.

theorem ofReal_integral_le_lintegral {α : Type uAlpha} [MeasurableSpace α]
    {μ : Measure α} {f : α → ℝ} {g : α → ℝ≥0∞}
    (hf : Integrable f μ) (hg : AEMeasurable g μ)
    (hle : ∀ᵐ x ∂μ, ENNReal.ofReal (f x) ≤ g x) :
    ENNReal.ofReal (∫ x, f x ∂μ) ≤ ∫⁻ x, g x ∂μ := by
…

theorem OAI.Problem356.Certificate.ae_eq_of_integral_certificate line 34

Source documentation

Equality with a signed lower certificate forces pointwise equality almost everywhere.

theorem ae_eq_of_integral_certificate {α : Type uAlpha} [MeasurableSpace α]
    {μ : Measure α} {f : α → ℝ} {g : α → ℝ≥0∞}
    (hf : Integrable f μ) (hg : AEMeasurable g μ)
    (hle : ∀ᵐ x ∂μ, ENNReal.ofReal (f x) ≤ g x)
    (hnonneg : 0 ≤ ∫ x, f x ∂μ)
    (heq : (∫⁻ x, g x ∂μ) = ENNReal.ofReal (∫ x, f x ∂μ)) :
    ∀ᵐ x ∂μ, g x = ENNReal.ofReal (f x) := by
…

def OAI.Problem356.Certificate.potentialSum line 56
Source documentation
The signed three-coordinate dual potential associated with one marginal potential.
```
def potentialSum (u : E3 → ℝ) (t : Triple) : ℝ :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple
theorem OAI.Problem356.Certificate.first_measurable line 59
theorem OAI.Problem356.Certificate.second_measurable line 60
theorem OAI.Problem356.Certificate.third_measurable line 61
theorem OAI.Problem356.Certificate.integrable_potentialSum line 64
Source documentation
Marginal identities transfer integrability of a signed potential to its sum.
```
theorem integrable_potentialSum {μ : Measure E3} {π : Measure Triple}
    (hπ : IsThreeCoupling μ π) {u : E3 → ℝ} (hu : Integrable u μ) :
    Integrable (potentialSum u) π := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.Certificate.potentialSum
theorem OAI.Problem356.Certificate.integral_potentialSum line 75
Source documentation
The integral of a common potential sum depends only on the common marginal.
```
theorem integral_potentialSum {μ : Measure E3} {π : Measure Triple}
    (hπ : IsThreeCoupling μ π) {u : E3 → ℝ} (hu : Integrable u μ) :
    (∫ t, potentialSum u t ∂π) = 3 * ∫ x, u x ∂μ := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.Certificate.potentialSum
theorem OAI.Problem356.Certificate.cost_measurable line 103
theorem OAI.Problem356.Certificate.coupling_ae_mem line 108
Source documentation
Every coupling is concentrated on the cube of any full-marginal-mass set.
```
theorem coupling_ae_mem {μ : Measure E3} {π : Measure Triple}
    (hπ : IsThreeCoupling μ π) {U : Set E3} (hU : ∀ᵐ x ∂μ, x ∈ U) :
    ∀ᵐ t ∂π, tripleFst t ∈ U ∧ tripleSnd t ∈ U ∧ tripleThd t ∈ U := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.tripleFst, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd
theorem OAI.Problem356.Certificate.kantorovich_lower_bound line 121
Source documentation
A signed supporting potential on a full-mass region is a Kantorovich lower bound.
```
theorem kantorovich_lower_bound {μ : Measure E3} {u : E3 → ℝ}
    (hu : Integrable u μ) {U : Set E3} (hU : ∀ᵐ x ∂μ, x ∈ U)
    (hcert : ∀ t : Triple, tripleFst t ∈ U → tripleSnd t ∈ U → tripleThd t ∈ U →
      ENNReal.ofReal (potentialSum u t) ≤ coulombCost t) :
    ENNReal.ofReal (3 * ∫ x, u x ∂μ) ≤ kantorovichValue μ := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.tripleFst, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd, OAI.Problem356.Certificate.potentialSum, OAI.Problem356.coulombCost, OAI.Problem356.kantorovichValue

theorem OAI.Problem356.Certificate.optimal_plan_of_certificate line 137

Source documentation

An explicit finite plan saturating a supporting potential is an optimizer.

theorem optimal_plan_of_certificate {μ : Measure E3} {π : Measure Triple}
    (hπ : IsThreeCoupling μ π) {u : E3 → ℝ}
    (hu : Integrable u μ) {U : Set E3} (hU : ∀ᵐ x ∂μ, x ∈ U)
    (hcert : ∀ t : Triple, tripleFst t ∈ U → tripleSnd t ∈ U → tripleThd t ∈ U →
      ENNReal.ofReal (potentialSum u t) ≤ coulombCost t)
    (heq : (∫⁻ t, coulombCost t ∂π) = ENNReal.ofReal (3 * ∫ x, u x ∂μ)) :
    (∫⁻ t, coulombCost t ∂π) = kantorovichValue μ ∧
      kantorovichValue μ < ⊤ ∧ KantorovichAttained μ := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.tripleFst, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd, OAI.Problem356.Certificate.potentialSum, OAI.Problem356.coulombCost, OAI.Problem356.kantorovichValue, OAI.Problem356.KantorovichAttained

theorem OAI.Problem356.Certificate.optimal_ae_contact line 155

Source documentation

Every optimal finite plan must lie on the equality set of a supporting potential.

theorem optimal_ae_contact {μ : Measure E3} {π : Measure Triple}
    (hπ : IsThreeCoupling μ π) {u : E3 → ℝ}
    (hu : Integrable u μ) {U : Set E3} (hU : ∀ᵐ x ∂μ, x ∈ U)
    (hcert : ∀ t : Triple, tripleFst t ∈ U → tripleSnd t ∈ U → tripleThd t ∈ U →
      ENNReal.ofReal (potentialSum u t) ≤ coulombCost t)
    (hnonneg : 0 ≤ 3 * ∫ x, u x ∂μ)
    (hvalue : kantorovichValue μ = ENNReal.ofReal (3 * ∫ x, u x ∂μ))
    (hopt : (∫⁻ t, coulombCost t ∂π) = kantorovichValue μ) :
    ∀ᵐ t ∂π, coulombCost t = ENNReal.ofReal (potentialSum u t) := by
…