RenyiLocalVariation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Localized power first variation with its actual energy density

theorem OAI.RegularPointCoordinates.path_renyi_smooth_variation line 15

theorem OAI.RegularPointCoordinates.renyi_core_path_set_variation line 48

Source documentation

The finite-dimensional power variation on a bounded path family is the integral of the genuine carré-du-champ, with the exact density power. Only the restricted family is bounded; the reference volume may be infinite.

theorem renyi_core_path_set_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