RegularActualPatches.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed actual patches and energy centers at every scale

def OAI.RegularPointCoordinates.RegularBilinearData.patchRadius line 24
def OAI.RegularPointCoordinates.RegularBilinearData.patchRegion line 27
def OAI.RegularPointCoordinates.RegularBilinearData.patchNet line 29
def OAI.RegularPointCoordinates.RegularBilinearData.patchCutoff line 31
def OAI.RegularPointCoordinates.RegularBilinearData.patchDomain line 35
theorem OAI.RegularPointCoordinates.regular_net_pinching_diameter_le line 41
Source documentation
The net is much finer than the directional pinching radius.
```
theorem regular_net_pinching_diameter_le {R : ℝ} (hR : 0 < R) (shift i : ℕ) :
    2 * 144 * regularNetRadius R shift i ≤ distanceSourceRadius R (shift + i) / 512 := by
…
```
Mentions: OAI.RegularPointCoordinates.regularNetRadius, OAI.RegularPointCoordinates.distanceSourceRadius
theorem OAI.RegularPointCoordinates.regular_actual_patch_cover line 53

theorem OAI.RegularPointCoordinates.exists_regular_actual_patch_centers line 69

Source documentation

Each operator center is fixed once for the entire active patch. The same center satisfies both the pinching estimate and the mass comparison distance bound; it is independent of the subsequently tested vector.

theorem exists_regular_actual_patch_centers {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {base : X} {a κ B J C A Cχ enlargement zeta eta Cpin budget : ℝ}
    {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
    (hzeta : zeta ≤ 1 / 64) (psi : EuclideanGevreyCutoff n)
    (f : RegularPinchingField e.heat Cpin budget) (hCpin : 0 ≤ Cpin) :
    ∃ center : ∀ i, {y : X // y ∈ e.heat.patchNet i} →
        {q : X // q ∈ ball base (e.heat.radius / 32)},
      ∀ i y,
        (center i y).val ∈ e.heat.patchDomain psi.value i y.val ∧
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.EuclideanGevreyCutoff, OAI.RegularPointCoordinates.RegularPinchingField

theorem OAI.RegularPointCoordinates.RegularPinchingField.shifted_energy_sum_le line 119
Source documentation
Starting the iteration at the heat shift preserves the total budget.
```
theorem shifted_energy_sum_le (f : RegularPinchingField d C budget)
    (q : {q : X // q ∈ ball base (d.radius / 32)}) (shift k : ℕ) :
    (∑ i ∈ Finset.range k, f.energy q (shift + i)) ≤ budget := by
…
```
Mentions: OAI.RegularPointCoordinates.RegularPinchingField