HarmonicGramSourceComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact source formula for the actual mean and heat Gram forms

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.mean_sub_heat_source line 23

Source documentation

Applying the genuine compact-source identity to the actual cutoff energy gives the mean-minus-heat formula, including its scalar regularizer.

theorem LocalHarmonicEnergy.mean_sub_heat_source
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ))
    (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
    (a : X) {R : ℝ} (hR : 0 < R)
    (hχR : ∀ z ∉ closedBall a R, χ z = 0)
    (hqR : ∀ᵐ z ∂μ, z ∉ closedBall a R → q z = 0)
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) (hχA : ∀ z ∈ A, χ z = 1)
    {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) (x : X) (lambda : ℝ) :
    ⟪v, (sobolevMeanGram μ hQ U A hA -
…

Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.sobolevMeanGram