HarmonicCurvatureBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual curvature-source integrals for the harmonic coordinate map

theorem OAI.RegularPointCoordinates.exists_harmonic_curvature_integral_bound line 25

Source documentation

The short- and long-time curvature pairings of the genuine cutoff energy have a uniform vanishing bound. The same constant works in every direction and does not depend on the working radius.

theorem exists_harmonic_curvature_integral_bound (hg : HasCoordinateHeatBounds μ ker)
    (hdiff : HasGaussianHeatDifferenceBounds μ ker)
    (n : ℕ) {A V W : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hW : 0 ≤ W) :
    ∃ C : ℝ, 0 < C ∧ ∀ (R : ℝ), 0 < R → R ≤ 1 → ∀ (i : ℕ) (x q : X),
      μ (ball q (R / 2 ^ i)) ≠ ∞ →
      V * (R / 2 ^ i) ^ n ≤ μ.real (ball q (R / 2 ^ i)) → dist x q ≤ A * (R / 2 ^ i) →
      (∀ j, μ.real (ball x (R / 2 ^ j)) ≤ W * (R / 2 ^ j) ^ n) →
      (∀ t, 0 < t → t ≤ R ^ 2 → ∀ z ∈ ball x R,
        V * (Real.sqrt t) ^ n ≤ μ.real (ball z (Real.sqrt t))) →
      ∀ (U : E →L[ℝ] SobolevSpace μ hQ) (M : PositiveBilinearMeasure X E)
        (κ : ℝ) (p : X) (r : ℝ) (L : ℝ≥0) (v : E)
        (_G : LocalHarmonicEnergy μ hQ U M κ p r L v) (χ : X →ᵇ ℝ),
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy