OAI/Geometry/RCD/Transport/MeasuredTransportData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded transport families supplied by compact Euclidean densities

  1. structure OAI.RegularPointCoordinates.MeasuredTransportData line 17

    Source documentation

    Bounded source measures, optimal transport plans, compression estimates, and convergence of their Euclidean pushforwards.

    structure MeasuredTransportData {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (p : ℕ → X) (r : ℕ → ℝ) (S τ : ℝ) (v : ℕ → X → Euclidean n)
    (α β : ProbabilityMeasure (Euclidean n)) (c₀ : ℝ) where
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.Euclidean

  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.measured_transport_data line 42