RegularPatchCenters.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed patch centers for the actual local mass matrices

theorem OAI.RegularPointCoordinates.RegularPinchingField.exists_patch_centers line 19

Source documentation

The positive energy floor chooses each patch center before its mass matrix is fixed. Thus the displacement bound uses the actual mean and Bochner mass at the chosen center, with no third-center hypothesis.

theorem RegularPinchingField.exists_patch_centers {K : ℝ} {n : ℕ}
    {hX : NoncollapsedRCD K n X} [(hausdorff n X).Regular]
    {base : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    {enlargement zeta C budget : ℝ} {d : RegularBilinearData hX base hk enlargement zeta}
    (f : RegularPinchingField d C budget) (hC : 0 ≤ C) (i : ℕ) {ι : Type*}
    (patch : ι → Set {q : X // q ∈ ball base (d.radius / 32)})
    (hne : ∀ j, (patch j).Nonempty)
    (hdiam : ∀ j, ∀ x ∈ patch j, ∀ z ∈ patch j,
      dist x.val z.val ≤ distanceSourceRadius d.radius i / 512) :
    ∃ center : ι → {q : X // q ∈ ball base (d.radius / 32)},
      ∀ j, center j ∈ patch j ∧
…

theorem OAI.RegularPointCoordinates.RegularPinchingField.exists_normalized_centers line 51

Source documentation

Apply the selection to the actual normalized cutoffs of a localized finite cover. The overlap radius controls the pair distance required by pinching; no regularity of the source energy is needed.

theorem RegularPinchingField.exists_normalized_centers {K : ℝ} {n : ℕ}
    {hX : NoncollapsedRCD K n X} [(hausdorff n X).Regular]
    {base : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    {enlargement zeta C budget : ℝ} {d : RegularBilinearData hX base hk enlargement zeta}
    (f : RegularPinchingField d C budget) (hC : 0 ≤ C) (i : ℕ)
    (A : Set X) (r : ℝ≥0) (T : X → Euclidean n →L[ℝ] Euclidean n)
    (psi : Euclidean n → ℝ) (s : Finset X) {N : ℕ} {L R : ℝ}
    (cover : IsLocalizedPatchCover A r d.values s (normalizedPatchCutoff r d.values T psi) N L R)
    (hzero : psi 0 = 1) (hA : A ⊆ ball base (d.radius / 32))
    (hsmall : 2 * L * (r : ℝ) ≤ distanceSourceRadius d.radius i / 512) :
    ∃ center : {y : X // y ∈ s} → {q : X // q ∈ ball base (d.radius / 32)},
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularBilinearData, OAI.RegularPointCoordinates.RegularPinchingField, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsLocalizedPatchCover, OAI.RegularPointCoordinates.normalizedPatchCutoff, OAI.RegularPointCoordinates.distanceSourceRadius