FirstCoordinateLift.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem356.FirstCoordinateLift.separated_replace_first line 17
Source documentation
Replacing only the first coordinate by a nearby point preserves half the separation, without any component-label hypothesis.
```
lemma separated_replace_first {η δ : ℝ} {t : Triple} {x : E3}
    (hη : 0 < η) (ht : Separated η t)
    (hclose : dist x t.1 ≤ δ) (hδ : δ ≤ η / 2) :
    Separated (η / 2) (x, t.2) := by
…
```
Mentions: OAI.Problem356.Triple, OAI.Problem356.E3
lemma OAI.Problem356.FirstCoordinateLift.separated_half line 29
Source documentation
Weakening separation to half its value.
```
lemma separated_half {η : ℝ} {t : Triple} (hη : 0 < η)
    (ht : Separated η t) : Separated (η / 2) t := by
…
```
Mentions: OAI.Problem356.Triple
lemma OAI.Problem356.FirstCoordinateLift.preserves_coordinates line 35
Source documentation
The two noncentral coordinates of a measure-valued lift preserve the marginal.
```
lemma preserves_coordinates {μ : Measure E3} {π : Measure Triple}
    (hπ : IsThreeCoupling μ π) {Q : E3 → Triple}
    (hQ : Measurable Q) (hmap : Measure.map Q μ = π) :
    Preserves μ (tripleSnd ∘ Q) ∧ Preserves μ (tripleThd ∘ Q) := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.Preserves, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd

theorem OAI.Problem356.FirstCoordinateLift.graph_cost_of_lift line 49

Source documentation

A lift of a separated coupling, whose first coordinate remains nearby, gives a finite-cost preserving pair and the quantitative Coulomb estimate.

theorem graph_cost_of_lift {μ : Measure E3} [IsProbabilityMeasure μ]
    {π : Measure Triple} (hπ : IsThreeCoupling μ π)
    {Q : E3 → Triple} (hQ : Measurable Q) (hmap : Measure.map Q μ = π)
    {η δ : ℝ} (hη : 0 < η) (hδ : δ ≤ η / 2)
    (hsep : ∀ᵐ t ∂π, Separated η t)
    (hclose : ∀ᵐ x ∂μ, dist x (Q x).1 ≤ δ) :
    Preserves μ (tripleSnd ∘ Q) ∧ Preserves μ (tripleThd ∘ Q) ∧
      graphCost μ (tripleSnd ∘ Q) (tripleThd ∘ Q) < ⊤ ∧
      graphCost μ (tripleSnd ∘ Q) (tripleThd ∘ Q) ≤
        (∫⁻ t, coulombCost t ∂π) + ENNReal.ofReal (24 * δ / η ^ 2) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.Preserves, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd, OAI.Problem356.graphCost, OAI.Problem356.coulombCost