OAI/Geometry/RCD/Transport/RenyiPathPrimitive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.renyi_path_integrable_of_bounds line 16
2. theorem OAI.RegularPointCoordinates.inverseInitialDensityPlan_compression_path line 37
3. theorem OAI.RegularPointCoordinates.path_renyi_signed_variation line 53

   Source documentation

   The local family requires bounded density only along its own paths. The represented primitive is the genuine Sobolev direction in the Kantorovich first variation.

   theorem path_renyi_signed_variation (π : Measure C(Time,X)) [IsFiniteMeasure π]
       (hgeo : ∀ᵐ γ ∂π, IsGeodesic γ) {C : ℝ≥0∞} (hC : C≠∞)
       (hcomp : ∀ t : Time, π.map (fun γ => γ t)≤C • μ)
       (hD : MemLp (fun γ : C(Time,X) => dist (γ 0) (γ 1)) 2 π)
       {D : ℝ} (hDb : ∀ᵐ γ ∂π, dist (γ 0) (γ 1)≤D)
       (u ρ v : SobolevSpace μ hQ) {ε M q : ℝ}
       (hε : 0<ε) (hq0 : 0<q) (hq1 : q<1)
       (hbound : ∀ t : Time, ∀ᵐ γ ∂π,
         ε≤SobolevSpace.toLp μ hQ ρ (γ t) ∧ SobolevSpace.toLp μ hQ ρ (γ t)≤M)
       (c : ℝ)
       (hv : ∀ t : Time, ∀ᵐ γ ∂π, SobolevSpace.toLp μ hQ v (γ t) =
         renyiDualPower q (SobolevSpace.toLp μ hQ ρ (γ t))-c)
   …

   Mentions: OAI.RegularPointCoordinates.Time, OAI.RegularPointCoordinates.IsGeodesic, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.renyiDualPower