OAI/Geometry/RCD/Transport/RenyiEnergyIntegrability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.integrable_positive_power_of_bounded line 13
2. theorem OAI.RegularPointCoordinates.memLp_density_power line 27
3. theorem OAI.RegularPointCoordinates.renyi_energy_integrable_of_relative_gradient line 40

   Source documentation

   The usual relative gradient estimate for a positive log-Lipschitz density makes the Rényi energy pairing integrable at every N >= 2.

   theorem renyi_energy_integrable_of_relative_gradient (u ρ : SobolevSpace μ hQ)
       (hp : ∀ᵐ x ∂μ, 0<SobolevSpace.toLp μ hQ ρ x)
       (hi : Integrable (SobolevSpace.toLp μ hQ ρ) μ) {M L q : ℝ}
       (hb : ∀ᵐ x ∂μ, SobolevSpace.toLp μ hQ ρ x≤M) (hq : 1/2≤q)
       (hrel : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ ρ x≤
         L*SobolevSpace.toLp μ hQ ρ x) :
       Integrable (fun x => (q-1)*(SobolevSpace.toLp μ hQ ρ x)^(q-1)*
         localGamma μ hQ u ρ x) μ := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.localGamma