RenyiGlobalVariation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Noncompact Rényi first variation by integrable path truncation

theorem OAI.RegularPointCoordinates.renyi_core_signed_variation line 18

Source documentation

Ordinary integrability of the explicit path majorant and weighted energy density suffices to remove all path truncations. No finite-volume or global positive lower bound is imposed on the density.

theorem renyi_core_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 π)
    (u ρ : SobolevSpace μ hQ)
    (hp : ∀ᵐ x ∂μ, 0<SobolevSpace.toLp μ hQ ρ x)
    {g : X → ℝ} {L : ℝ≥0} (hg : LipschitzWith L g)
    (hlog : (fun x => Real.log (SobolevSpace.toLp μ hQ ρ x)) =ᵐ[μ] g)
    (h0 : π.map (fun γ => γ 0)=μ.withDensity
      (fun x => ENNReal.ofReal (SobolevSpace.toLp μ hQ ρ x)))
    {φ ψ : X → ℝ} (hu : φ=ᵐ[μ] SobolevSpace.toLp μ hQ u)
…

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