ScaledFixedCutoffNeighborhood.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A regular-neighborhood cutoff with a uniform starting index

theorem OAI.RegularPointCoordinates.half_volume_upper line 15
theorem OAI.RegularPointCoordinates.exists_scaled_fixed_cutoff_neighborhood_with_source line 28
Source documentation
The cutoff constant and starting index are fixed before the radius, coordinate map or full Bochner measure is chosen. Only local calculus and the displayed regular-neighborhood volume bounds are used.
```
theorem exists_scaled_fixed_cutoff_neighborhood_with_source {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    (hn : 2 ≤ n)
    (hhessian : LocalPoissonHessianInput hX) (hproduct : LocalPoissonGradientProductInput hX)
    (hcutoff : LocalGoodCutoffInput hX)
    {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
    (hg : HasCoordinateHeatBounds (hausdorff n X) ker) {omega : ℝ} (homega : 0 < omega) :
    ∃ C A : ℝ, 1 ≤ C ∧ 0 ≤ A ∧
      (∀ p s, 0 < s → -1 ≤ K * s ^ 2 →
        Nonempty (GoodLaplacianCutoff (hausdorff n X) hX.quadratic p s C)) ∧
      ∃ J : ℕ, ∀ (R : ℝ), 0 < R → R ≤ 1 →
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.LocalGoodCutoffInput, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.GoodLaplacianCutoff
theorem OAI.RegularPointCoordinates.exists_scaled_fixed_cutoff_neighborhood line 127
Source documentation
The cutoff constant and starting index are fixed before the radius, coordinate map or full Bochner measure is chosen. Only local calculus and the displayed regular-neighborhood volume bounds are used.
```
theorem exists_scaled_fixed_cutoff_neighborhood {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    (hn : 2 ≤ n)
    (hhessian : LocalPoissonHessianInput hX) (hproduct : LocalPoissonGradientProductInput hX)
    (hcutoff : LocalGoodCutoffInput hX)
    {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
    (hg : HasCoordinateHeatBounds (hausdorff n X) ker) {omega : ℝ} (homega : 0 < omega) :
    ∃ C : ℝ, 1 ≤ C ∧ ∃ J : ℕ, ∀ (R : ℝ), 0 < R → R ≤ 1 →
      |K| * (16 * R) ^ 2 ≤ 1 → ∀ (p : X) (L : ℝ≥0)
      (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
      (M : PositiveBilinearMeasure X (Euclidean n)),
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalPoissonGradientProductInput, OAI.RegularPointCoordinates.LocalGoodCutoffInput, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean