PointedPlanCost.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact quadratic-cost transfer through the prescribed approximation maps

theorem OAI.RegularPointCoordinates.pointed_plan_cost_error line 16

theorem OAI.RegularPointCoordinates.pointed_plan_cost_tendsto line 62

Source documentation

The actual rescaled source costs converge to the cost of the same limiting endpoint law; no optimality or continuity of the approximation maps is needed.

theorem pointed_plan_cost_tendsto {n : ℕ} {S ρ B : ℝ}
    (hρ : 0≤ρ) (hρS : ρ≤S) (hB : 0≤B)
    (p : ℕ → X) (r ε : ℕ → ℝ) (v : ℕ → X → Euclidean n)
    (hr : ∀ k, 0<r k) (hε : ∀ k, 0≤ε k) (hεlim : Tendsto ε atTop (𝓝 0))
    (hv : ∀ k, IsPointedApproximation (p k) 0 (r k) S (ε k) (v k))
    (hm : ∀ k, Measurable (v k)) (P : ℕ → ProbabilityMeasure C(Time,X))
    (h0 : ∀ k, ∀ᵐ γ ∂(P k : Measure C(Time,X)), dist (γ 0) (p k)≤ρ*r k)
    (h1 : ∀ k, ∀ᵐ γ ∂(P k : Measure C(Time,X)), dist (γ 1) (p k)≤ρ*r k)
    {Q : ProbabilityMeasure (Euclidean n × Euclidean n)}
    (hpair : Tendsto (fun k => (P k).map (fun γ => (v k (γ 0),v k (γ 1)))) atTop (𝓝 Q))
    (hbs : ∀ k, ∀ᵐ z ∂((P k).map (fun γ => (v k (γ 0),v k (γ 1))) :
        Measure (Euclidean n × Euclidean n)),
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.Time