OAI/Geometry/RCD/Coordinates/RegularShiftedCentralMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Central cumulative comparison at the interior heat scale

  1. theorem OAI.RegularPointCoordinates.RegularBilinearData.shifted_central_mass_comparison line 26

    Source documentation

    Discarding seventeen initial terms changes only a uniform finite constant. Both inequalities concern the actual heat inverse and central Bochner masses at the same interior scales.

    theorem shifted_central_mass_comparison :
    ∃ T : ℝ, 0 < T ∧ ∀ q, q ∈ ball base (d.radius / 32) → ∀ (xi : Euclidean n) (k : ℕ),
      let Q := fun i => d.heatAt q (d.shift + i + 17)
…

    Mentions: OAI.RegularPointCoordinates.Euclidean