OAI/Geometry/RCD/Harmonic/GramSourceEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual mean/heat discrepancy in the three source budgets

  1. theorem OAI.RegularPointCoordinates.three_source_triangle line 14
  2. theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.mean_sub_heat_norm_le line 39

    Source documentation

    The actual metric discrepancy is bounded by the terminal heat value, regularizer, full positive-source integrals, curvature integrals and annular error integrals. No comparison estimate is assumed.

    theorem LocalHarmonicEnergy.mean_sub_heat_norm_le (hρ : 0 < ρ) (hρr : ρ < r)
    (A : Set X) (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A)
    (hχA : ∀ z ∈ A, χ.weight z = 1) {s t : ℝ} (hs : 0 < s) (hst : s ≤ t)
    (x : X) (lambda : ℝ) :
    let f := SobolevSpace.toLp μ hQ (G.cutoffEnergy μ hQ χ.weight χ.sobolev)
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace.toLp