RegularPatchMassSum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite patch mass sums and the reverse central-ball covering

theorem OAI.RegularPointCoordinates.RegularBilinearData.raw_patch_mass_sum_le line 24

Source documentation

The heat-envelope total controls the full raw mass of every finite family of sufficiently nearby patches at the moving inverse vectors.

theorem raw_patch_mass_sum_le {q : X} (hq : q ∈ ball base (d.radius / 32))
    {ι : Type*} (s : ℕ → Finset ι)
    (centers : ℕ → ι → X) (N : ℕ) (hcard : ∀ i, (s i).card ≤ N)
    (hroom : ∀ i y, y ∈ s i → dist (centers i y) q ≤
      (d.radius / (2 : ℝ) ^ (d.shift + i + 15)) / 12)
    (xi : Euclidean n) (k : ℕ) :
    let Q := fun i => d.heatAt q (d.shift + i + 17)
…

Mentions: OAI.RegularPointCoordinates.Euclidean

def OAI.RegularPointCoordinates.patchCentralFactor line 76
Source documentation
The precise scale factor for the strictly interior central mass.
```
def patchCentralFactor (n : ℕ) : ℝ := (65536 : ℝ) ^ 2 / (65536 : ℝ) ^ n
…
```

theorem OAI.RegularPointCoordinates.rawPinchingMass_covers_central line 81

Source documentation

A center within one twelfth of the mean radius has a mass ball that covers the central ball two scales below the mean radius.

theorem rawPinchingMass_covers_central {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (M : PositiveBilinearMeasure X E) (n : ℕ) {R : ℝ} (hR : 0 < R)
    {q z : X} (i : ℕ) (hroom : dist z q ≤ (R / (2 : ℝ) ^ (i + 15)) / 12) (v : E) :
    patchCentralFactor n * ⟪v, dyadicBochnerMass M n q R (i + 17) v⟫_ℝ ≤
      ⟪v, rawPinchingMass M n R z i v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.patchCentralFactor, OAI.RegularPointCoordinates.dyadicBochnerMass, OAI.RegularPointCoordinates.rawPinchingMass