LongTimeMassSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Summing every long-time block in the original full-mass envelope

theorem OAI.RegularPointCoordinates.dyadic_radius_ratio line 15

theorem OAI.RegularPointCoordinates.exists_long_time_mass_sum_bound line 29

Source documentation

All long-time blocks sum to a fixed multiple of the same envelope used by the heat decrement, with the original full Bochner measure.

theorem exists_long_time_mass_sum_bound (hg : HasCoordinateHeatBounds μ ker)
    (hdiff : HasGaussianHeatDifferenceBounds μ ker)
    (m : ℕ) {A V : ℝ} (hA : 0 ≤ A) (hV : 0 < V) :
    ∃ C : ℝ, 0 < C ∧ ∀ (M : PositiveBilinearMeasure X (Euclidean (m + 2)))
      (R : ℝ) (_hR : 0 < R), R ≤ 1 → ∀ (x : X) (χ : X →ᵇ ℝ),
      ∀ hc : HasCompactSupport (χ : X → ℝ), (∀ z, 0 ≤ χ z ∧ χ z ≤ 1) →
      (∀ z ∉ ball x R, χ z = 0) → ∀ (i : ℕ) (q : X),
      μ (ball q (R / 2 ^ i)) ≠ ∞ → 0 < μ.real (ball q (R / 2 ^ i)) →
      dist x q ≤ A * (R / 2 ^ i) →
      (∀ t, 0 < t → t ≤ R ^ 2 →
        ∀ z, χ z ≠ 0 → V * (Real.sqrt t) ^ (m + 2) ≤ μ.real (ball z (Real.sqrt t))) →
      ∀ v : Euclidean (m + 2),
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean