RescaledTransportPotentials.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Scale-invariant potentials for bounded endpoint transport

theorem OAI.RegularPointCoordinates.rescaled_transport_potentials line 16

Source documentation

The linear-radius potential theorem has uniform constants after rescaling. Only its value bounds, dual inequality and exact contact are retained here.

theorem rescaled_transport_potentials (μ : Measure X) [IsFiniteMeasureOnCompacts μ]
    (hQ : QuadraticCheegerEnergy μ) (hgeo : IsGeodesicSpace X)
    (ν₀ ν₁ : Measure X) [IsProbabilityMeasure ν₀] [IsProbabilityMeasure ν₁]
    (hac : ν₀ ≪ μ) {π : Measure (X×X)} (hp : IsOptimalCoupling ν₀ ν₁ π)
    (p : X) {ρ r : ℝ} (hρ : 0≤ρ) (hr : 0<r)
    (h0 : ∀ᵐ x ∂ν₀, dist x p≤ρ*r) (h1 : ∀ᵐ x ∂ν₁, dist x p≤ρ*r) :
    ∃ φ ψ : X → ℝ,
      LipschitzWith ⟨5*ρ/r,by positivity⟩ φ ∧
      LipschitzWith ⟨5*ρ/r,by positivity⟩ ψ ∧
      (∀ x, |φ x|≤10*ρ^2) ∧ (∀ x, |ψ x|≤10*ρ^2) ∧
      (∀ x y, φ x+ψ y≤(dist x y/r)^2/2) ∧
      (∀ᵐ xy ∂π, φ xy.1+ψ xy.2=(dist xy.1 xy.2/r)^2/2) := by
…

Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.IsGeodesicSpace, OAI.RegularPointCoordinates.IsOptimalCoupling