OAI/Geometry/RCD/Transport/RenyiSobolev.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.renyiDualClip line 12
2. theorem OAI.RegularPointCoordinates.renyiDualClip_zero line 15
3. theorem OAI.RegularPointCoordinates.renyiDualClip_lipschitz line 18
4. def OAI.RegularPointCoordinates.SobolevSpace.renyiDual line 45
5. theorem OAI.RegularPointCoordinates.SobolevSpace.renyiDual_coe line 50
6. theorem OAI.RegularPointCoordinates.planInitialSecant_sub_const line 62
7. theorem OAI.RegularPointCoordinates.reference_renyi_signed_variation line 75

   Source documentation

   The finite power first variation is the energy pairing with the constructed Sobolev primitive. No derivative of a density representative is used on exceptional sets.

   theorem reference_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 ρ : SobolevSpace μ hQ) {ε q : ℝ} (hε : 0<ε) (hq0 : 0<q) (hq1 : q<1)
       (hl : ∀ᵐ x ∂μ, ε≤SobolevSpace.toLp μ hQ ρ x)
       (h0 : π.map (fun γ => γ 0)=μ.withDensity
         (fun x => ENNReal.ofReal (SobolevSpace.toLp μ hQ ρ x)))
       {φ ψ : X → ℝ} (hu : φ=ᵐ[μ] SobolevSpace.toLp μ hQ u)
       (had : ∀ x y, φ x+ψ y≤dist x y^2/2)
   …

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