The Geometry of Optimal Transport

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def IsAbsolutelyContinuousMetricCurve
    {M : Type*} [PseudoMetricSpace M]
    (curve : ℝ → M) : Prop :=
  ∀ᵐ t ∂(by volume_tac : Measure ℝ),
    ∃ speed : ℝ, HasMetricDerivativeAt curve speed t

end MetricCurve
end Geometry
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def IsAlphaGeodesicallyConvex
    {M : Type*} [MetricSpace M]
    (isGeodesic : (ℝ → M) → Prop) (F : M → ℝ) (alpha : ℝ) : Prop :=
  ∀ path : ℝ → M, isGeodesic path →
    ∀ t : ℝ, t ∈ Icc (0 : ℝ) 1 →
      F (path t) ≤
        (1 - t) * F (path 0) + t * F (path 1) -
          (alpha * t * (1 - t) / 2) * dist (path 0) (path 1) ^ 2

/-- The chord formulation of geodesic alpha-convexity implies its first-order
form along a differentiable selected geodesic.  The scalar
`gradientPairing` is the derivative of `F` along the path at its initial
point; identifying it with the Riemannian or Wasserstein gradient pairing is
a separate geometric theorem.

This is the one-dimensional limiting argument behind Chewi display
(1.4.7). -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def dualTransportValue
    {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]
    (cost : E × F → ℝ) (mu : Measure E) (nu : Measure F) : ℝ :=
  sSup {r : ℝ | ∃ (f : E → ℝ) (g : F → ℝ),
    DualFeasible cost mu nu f g ∧
      r = (∫ x, f x ∂mu) + ∫ y, g y ∂nu}

/-- Chewi display (1.3.7): source-facing expansion of the dual value. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem dualTransportValue_eq_sSup
    {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]
    (cost : E × F → ℝ) (mu : Measure E) (nu : Measure F) :
    dualTransportValue cost mu nu =
      sSup {r : ℝ | ∃ (f : E → ℝ) (g : F → ℝ),
        DualFeasible cost mu nu f g ∧
          r = (∫ x, f x ∂mu) + ∫ y, g y ∂nu} :=
  rfl

end KantorovichDual
end Measure
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def wassersteinDistance
    {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]
    (μ ν : Measure E) : ℝ≥0∞ :=
  (Transport.transportCost (quadraticCost (E := E)) μ ν) ^ (1 / 2 : ℝ)

/-- Chewi display (1.3.5): the square of `W₂` is the infimum of the
quadratic costs over all couplings. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem wassersteinDistance_sq
    {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]
    (μ ν : Measure E) :
    wassersteinDistance μ ν ^ 2 =
      Transport.transportCost (quadraticCost (E := E)) μ ν := by
  rw [wassersteinDistance, ← ENNReal.rpow_two, ← ENNReal.rpow_mul]
  norm_num

/-- Every concrete coupling bounds the squared Wasserstein distance from
above by its quadratic transport cost.

This is the source-facing bridge used before proving optimal-plan existence or
constant-speed displacement geodesics. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def IsAbsolutelyContinuousFiniteSecondMoment
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) : Prop :=
  IsProbabilityMeasure μ ∧
    μ ≪ (volume : Measure E) ∧
    Integrable (fun x : E => ‖x‖ ^ 2) μ

/-- Expansion of the three conditions in the `P₂,ac` definition. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def IsWassersteinGeodesic
    (μ₀ μ₁ : Measure E) (curve : ℝ → Measure E) : Prop :=
  WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₀ ∧
    WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₁ ∧
    ∃ γ : Measure (E × E),
      IsQuadraticOptimalCoupling γ μ₀ μ₁ ∧
      ∀ t ∈ Icc (0 : ℝ) 1,
        curve t = displacementInterpolation γ t

/-- An optimal coupling and two `P₂,ac` endpoints generate the source
displacement-interpolation predicate. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def transportCost {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (c : α × β → ℝ≥0∞) (μ : Measure α) (ν : Measure β) : ℝ≥0∞ :=
  sInf {r : ℝ≥0∞ | ∃ γ ∈ couplingSet μ ν, r = ∫⁻ z, c z ∂γ}

/-- Source-facing expansion of the Kantorovich value in display (1.3.2). -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem transportCost_eq_sInf
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (c : α × β → ℝ≥0∞) (μ : Measure α) (ν : Measure β) :
    transportCost c μ ν =
      sInf {r : ℝ≥0∞ | ∃ γ ∈ couplingSet μ ν, r = ∫⁻ z, c z ∂γ} :=
  rfl

/-- Every feasible coupling gives an upper bound on the Kantorovich optimum.

This is the basic `sInf <= candidate` edge used repeatedly when a concrete
coupling is constructed (for example from a displacement interpolation or a
Markovian coupling).  It does not require existence of an optimizer. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem isProbabilityMeasure_of_isCoupling_left
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    {γ : Measure (α × β)} {μ : Measure α} {ν : Measure β}
    [IsProbabilityMeasure μ] (hγ : IsCoupling γ μ ν) :
    IsProbabilityMeasure γ := by
  constructor
  rw [← Measure.fst_univ, hγ.1, measure_univ]

/-- The independent product measure is a coupling of two probability measures.
This supplies the canonical nonemptiness witness for the Kantorovich feasible
set in Chewi, Definition 1.3.1. -/

Exact module and namespace context

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem isCoupling_prod {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (μ : Measure α) (ν : Measure β) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
    IsCoupling (μ.prod ν) μ ν := by
  constructor <;> simp

/-- The feasible set in the Kantorovich problem is nonempty for probability
marginals. -/

Exact module and namespace context