ScaledUniformCutoff.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A cutoff starting index chosen before the neighborhood radius

theorem OAI.RegularPointCoordinates.exists_scaled_cutoff_error_index line 24

Source documentation

A scale-normalized L1 source bound gives a uniform dyadic cutoff index. The source bound is supplied by harmonic_cutoff_scaled_L1 for the actual harmonic coordinates, using the already stated local calculus.

theorem exists_scaled_cutoff_error_index (n : ℕ) (hg : HasCoordinateHeatBounds μ ker)
    {A V : ℝ} (hA : 0 ≤ A) (hV : 0 < V) :
    ∃ J : ℕ, ∀ (R : ℝ) (_hR : 0 < R), R ≤ 1 → ∀ (p : X) (r κ C : ℝ) (L : ℝ≥0)
      (U : Euclidean n →L[ℝ] SobolevSpace μ hQ)
      (M : PositiveBilinearMeasure X (Euclidean n))
      (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v)
      (χ : GoodLaplacianCutoff μ hQ p (3 * R / 8) C),
      (∀ v : Euclidean n, ‖v‖ ≤ 2 →
        R ^ 2 * (∫ z, |cutoffSourceDensity μ hQ (G v).energy χ.sobolev χ.laplacian z| ∂μ) ≤
          A * R ^ n) →
      (∀ y, 3 * R / 8 ≤ dist p y → dist p y ≤ 3 * R / 4 →
        ∀ s, 0 < s → s ≤ R → V * s ^ n ≤ μ.real (ball y s)) →
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.cutoffSourceDensity