PatchCoverData.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Localized finite patch data from a uniform volume regime

The centers form a maximal finite net. Cutoffs are affine pullbacks of a fixed Euclidean cutoff. The half-error volume regime, coarse separation, and slow normalization growth bound the overlap. The smooth cutoff has core radius two and support radius three.

def OAI.RegularPointCoordinates.normalizedPatchCutoff line 34
Source documentation
The coordinate cutoff centered at a point of the original metric space.
```
def normalizedPatchCutoff (r : ℝ) (u : X → E) (T : X → E →L[ℝ] F)
    (psi : F → ℝ) (y : X) (P : E) : ℝ :=
…
```
def OAI.RegularPointCoordinates.normalizedPatchDomain line 39
Source documentation
The original-space active domain for one actual normalized cutoff.
```
def normalizedPatchDomain (A : Set X) (r : ℝ) (u : X → E)
    (T : X → E →L[ℝ] F) (psi : F → ℝ) (y : X) : Set X :=
…
```

theorem OAI.RegularPointCoordinates.self_mem_normalizedPatchDomain line 45

Source documentation

Every chosen net center belongs to its own active patch.

theorem self_mem_normalizedPatchDomain (A : Set X) (r : ℝ) (u : X → E)
    (T : X → E →L[ℝ] F) (psi : F → ℝ) {y : X} (hy : y ∈ A)
    (hzero : psi 0 = 1) : y ∈ normalizedPatchDomain A r u T psi y := by
…

Mentions: OAI.RegularPointCoordinates.normalizedPatchDomain

def OAI.RegularPointCoordinates.patchLocalizationFactor line 55
Source documentation
The metric radius forced by the normalized support and coarse separation.
```
def patchLocalizationFactor (c M L : ℝ) : ℝ := max 1 ((M * L / c) ^ 2)
```
theorem OAI.RegularPointCoordinates.patchLocalizationFactor_ge_one line 57

theorem OAI.RegularPointCoordinates.normalized_pair_norm_estimate line 62

Source documentation

Undoing the physical scaling in a pointed coordinate approximation gives the actual frozen displacement estimate.

theorem normalized_pair_norm_estimate (u : X → E) (T : E →L[ℝ] F)
    (x y : X) {t R delta : ℝ} (ht : 0 < t) (hR : 0 ≤ R)
    (hpoint : IsPointedApproximation y (0 : F) t R delta
      (fun z => t⁻¹ • T (u z - u y)))
    (hxy : dist x y ≤ R * t) :
    |‖T (u x - u y)‖ - dist x y| ≤ delta * t := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.normalized_near_pair_le line 83

Source documentation

Approximation at four times the fine radius supplies the core-two near-pair hypothesis of the finite patch construction.

theorem normalized_near_pair_le (u : X → E) (T : E →L[ℝ] F)
    (x y : X) {r : ℝ} (hr : 0 < r)
    (hpoint : IsPointedApproximation y (0 : F) (4 * r) (1 / 2) (1 / 4)
      (fun z => (4 * r)⁻¹ • T (u z - u y)))
    (hxy : dist x y ≤ r) : ‖T (u x - u y)‖ ≤ 2 * r := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.normalized_coarse_pair_lower line 95

Source documentation

A coarse pointed approximation at the pair scale supplies a fixed positive separation coefficient, independently of the pair distance.

theorem normalized_coarse_pair_lower (u : X → E) (T : E →L[ℝ] F)
    (x y : X) (hxy : x ≠ y)
    (hpoint : IsPointedApproximation y (0 : F) (4 * dist x y) (1 / 2) (1 / 8)
      (fun z => (4 * dist x y)⁻¹ • T (u z - u y))) :
    (1 / 2) * dist x y ≤ ‖T (u x - u y)‖ := by
…

Mentions: OAI.RegularPointCoordinates.IsPointedApproximation

def OAI.RegularPointCoordinates.patchOverlapBound line 107
Source documentation
A dimensional overlap bound in the half-error volume regime.
```
def patchOverlapBound (n : ℕ) (c M L : ℝ) : ℕ :=
…
```
structure OAI.RegularPointCoordinates.IsLocalizedPatchCover line 112
Source documentation
Concrete geometric and smoothness properties needed before assigning positive operators and energy centers to the finite patches.
```
structure IsLocalizedPatchCover (A : Set X) (r : ℝ≥0) (u : X → E)
    (s : Finset X) (phi : X → E → ℝ) (N : ℕ) (C L : ℝ) : Prop where
…
```
theorem OAI.RegularPointCoordinates.IsLocalizedPatchCover.one_le_cutoff_sum line 132
Source documentation
The actual cutoff sum is positive throughout the covered domain.
```
theorem one_le_cutoff_sum (d : IsLocalizedPatchCover A r u s phi N C L)
    {x : X} (hx : x ∈ A) : 1 ≤ ∑ y ∈ s, phi y (u x) := by
…
```
Mentions: OAI.RegularPointCoordinates.IsLocalizedPatchCover
theorem OAI.RegularPointCoordinates.IsLocalizedPatchCover.cutoff_sum_le line 141
Source documentation
The same sum is bounded by the geometric overlap constant: inactive terms vanish, so the total number of net points never enters the bound.
```
theorem cutoff_sum_le (d : IsLocalizedPatchCover A r u s phi N C L)
    {x : X} (hx : x ∈ A) : (∑ y ∈ s, phi y (u x)) ≤ N := by
…
```
Mentions: OAI.RegularPointCoordinates.IsLocalizedPatchCover
theorem OAI.RegularPointCoordinates.IsLocalizedPatchCover.support_inter_image_subset line 158
Source documentation
Active support, restricted to the actual coordinate image, comes from points in a uniformly enlarged original metric ball.
```
theorem support_inter_image_subset (d : IsLocalizedPatchCover A r u s phi N C L)
    {y : X} (hy : y ∈ s) :
    tsupport (phi y) ∩ u '' A ⊆ u '' (A ∩ closedBall y (C * r)) := by
…
```
Mentions: OAI.RegularPointCoordinates.IsLocalizedPatchCover
theorem OAI.RegularPointCoordinates.IsLocalizedPatchCover.active_card_of_mem_image line 166
Source documentation
The overlap bound in the exact coordinate-domain form used by PatchIterationGeometry.active_card. No injectivity is needed here.
```
theorem active_card_of_mem_image (d : IsLocalizedPatchCover A r u s phi N C L)
    {P : E} (hP : P ∈ u '' A) :
    (s.filter (fun y => P ∈ tsupport (phi y))).card ≤ N := by
…
```
Mentions: OAI.RegularPointCoordinates.IsLocalizedPatchCover

theorem OAI.RegularPointCoordinates.exists_normalized_patch_energy_centers line 185

Source documentation

The actual active domains supply the nonemptiness needed to choose fixed energy centers. They remain in the original bounded domain and the localized metric ball, and their affine displacement obeys the required three-times pair-energy bound at every active point.

theorem exists_normalized_patch_energy_centers
    (A : Set X) (r : ℝ≥0) (u : X → E) (T : X → E →L[ℝ] F)
    (psi : F → ℝ) (s : Finset X) {N : ℕ} {C L D floor : ℝ}
    (d : IsLocalizedPatchCover A r u s (normalizedPatchCutoff r u T psi) N C L)
    (hzero : psi 0 = 1) (energy : X → ℝ) (hfloor : 0 < floor)
    (hlower : ∀ x ∈ A, floor ≤ energy x)
    (op : X → E →L[ℝ] E) (hD : 0 ≤ D)
    (hpair : ∀ y ∈ s, ∀ x ∈ normalizedPatchDomain A r u T psi y,
      ∀ z ∈ normalizedPatchDomain A r u T psi y,
      ⟪u x - u z, op y (u x - u z)⟫_ℝ ≤
        D * (r : ℝ) ^ 2 * (energy x + energy z)) :
    ∃ center : X → X, ∀ y ∈ s,
…

Mentions: OAI.RegularPointCoordinates.IsLocalizedPatchCover, OAI.RegularPointCoordinates.normalizedPatchCutoff, OAI.RegularPointCoordinates.normalizedPatchDomain

theorem OAI.RegularPointCoordinates.half_volume_bounds line 223
Source documentation
The half-error relative-volume estimate gives the two bounds used by the packing argument, with their common Euclidean volume factor explicit.
```
theorem half_volume_bounds {V omega r : ℝ} {n : ℕ}
    (homega : 0 < omega) (hr : 0 < r)
    (hvolume : |V / (omega * r ^ n) - 1| ≤ 1 / 2) :
    (omega / 2) * r ^ n ≤ V ∧ V ≤ (3 * omega / 2) * r ^ n := by
…
```

theorem OAI.RegularPointCoordinates.maximal_normalized_patch_cover line 244

Source documentation

The actual maximal net and affine cutoff satisfy localization, weight-one covering and a scale-independent overlap bound. The measure premise is only the uniform half-error ball-volume estimate.

theorem maximal_normalized_patch_cover
    (μ : Measure X) (A : Set X) (hA : TotallyBounded A)
    (r : ℝ≥0) (hr : 0 < r) (u : X → E) (T : X → E →L[ℝ] F)
    (psi : F → ℝ) (n : ℕ) {R omega c M L : ℝ}
    (homega : 0 < omega) (hc : 0 < c) (hL : 2 ≤ L)
    (hscale : (patchLocalizationFactor c M L + 1) * r ≤ R)
    (hvolume : ∀ x ∈ A, ∀ t : ℝ, 0 < t → t ≤ R →
      |μ.real (ball x t) / (omega * t ^ n) - 1| ≤ 1 / 2)
    (hfinite : ∀ x t, μ (ball x t) ≠ (⊤ : ℝ≥0∞))
    (hsmooth : ContDiff ℝ ∞ psi)
    (hzero : ∀ z, 0 ≤ psi z) (hone : ∀ z, psi z ≤ 1)
    (hcore : ∀ z, ‖z‖ ≤ 2 → psi z = 1)
…

Mentions: OAI.RegularPointCoordinates.patchLocalizationFactor

theorem OAI.RegularPointCoordinates.bounded_maximal_normalized_patch_cover line 308

Source documentation

Properness is only used to turn a bounded, possibly nonclosed domain into the totally bounded set required for the actual finite net.

theorem bounded_maximal_normalized_patch_cover [ProperSpace X]
    (μ : Measure X) (A : Set X) (hA : Bornology.IsBounded A)
    (r : ℝ≥0) (hr : 0 < r) (u : X → E) (T : X → E →L[ℝ] F)
    (psi : F → ℝ) (n : ℕ) {R omega c M L : ℝ}
    (homega : 0 < omega) (hc : 0 < c) (hL : 2 ≤ L)
    (hscale : (patchLocalizationFactor c M L + 1) * r ≤ R)
    (hvolume : ∀ x ∈ A, ∀ t : ℝ, 0 < t → t ≤ R →
      |μ.real (ball x t) / (omega * t ^ n) - 1| ≤ 1 / 2)
    (hfinite : ∀ x t, μ (ball x t) ≠ (⊤ : ℝ≥0∞))
    (hsmooth : ContDiff ℝ ∞ psi)
    (hzero : ∀ z, 0 ≤ psi z) (hone : ∀ z, psi z ≤ 1)
    (hcore : ∀ z, ‖z‖ ≤ 2 → psi z = 1)
…

Mentions: OAI.RegularPointCoordinates.patchLocalizationFactor

theorem OAI.RegularPointCoordinates.normalized_patch_cover_of_pointed_approximations line 334

Source documentation

The coordinate premises can be stated as actual pointed approximations and slow norm growth. Their separation and near-pair consequences are derived before constructing the localized patch cover.

theorem normalized_patch_cover_of_pointed_approximations [ProperSpace X]
    (μ : Measure X) (A : Set X) (hA : Bornology.IsBounded A)
    (r : ℝ≥0) (hr : 0 < r) (u : X → E) (T : X → E →L[ℝ] F)
    (psi : F → ℝ) (n : ℕ) {R omega M L exponent : ℝ}
    (homega : 0 < omega) (hM : 0 ≤ M) (hL : 2 ≤ L) (hexponent : exponent ≤ 1 / 2)
    (hscale : (patchLocalizationFactor (1 / 2) M L + 1) * r ≤ R)
    (hvolume : ∀ x ∈ A, ∀ t : ℝ, 0 < t → t ≤ R →
      |μ.real (ball x t) / (omega * t ^ n) - 1| ≤ 1 / 2)
    (hfinite : ∀ x t, μ (ball x t) ≠ (⊤ : ℝ≥0∞))
    (hsmooth : ContDiff ℝ ∞ psi)
    (hzero : ∀ z, 0 ≤ psi z) (hone : ∀ z, psi z ≤ 1)
    (hcore : ∀ z, ‖z‖ ≤ 2 → psi z = 1)
…

Mentions: OAI.RegularPointCoordinates.patchLocalizationFactor

def OAI.RegularPointCoordinates.patchCoreBump line 375
Source documentation
An actual smooth core-two, support-three cutoff on the coordinate space.
```
def patchCoreBump : ContDiffBump (0 : F) := ⟨2, 3, by norm_num, by norm_num⟩
```
theorem OAI.RegularPointCoordinates.patchCoreBump_properties line 377
theorem OAI.RegularPointCoordinates.exists_regular_patch_cover_radius line 403
Source documentation
The published volume convergence, Bishop--Gromov and density inputs give one working neighborhood and one uniform overlap constant for every smaller-scale normalized patch family. The remaining premises concern only the coordinate normalizations: near-pair control and coarse separation with slow growth. No patch conclusion is assumed.
```
theorem exists_regular_patch_cover_radius
    (μ : Measure X) (m : ℕ) {p : X} {a omega rho c M : ℝ}
    (ha : 0 ≤ a) (homega : 0 < omega) (hrho : 0 < rho) (hc : 0 < c)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular (m + 1) p)
    (hvolume : EuclideanRescalingVolumeConvergence μ (m + 1) p omega)
    (hcomparison : BallVolumeComparison μ (comparisonModelVolume m a))
    (hdensity : ∀ y, SmallScaleVolumeUpper μ (comparisonModelVolume m a) y omega)
    (hfinite : ∀ y t, μ (ball y t) ≠ (⊤ : ℝ≥0∞)) :
    ∃ R : ℝ, 0 < R ∧ R ≤ rho ∧
      ∀ (r : ℝ≥0), 0 < r → (patchLocalizationFactor c M 3 + 1) * r ≤ R →
      ∀ (u : X → E) (T : X → E →L[ℝ] F),
      (∀ x ∈ ball p R, ∀ y ∈ ball p R, dist x y ≤ r →
…
```
Mentions: OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SmallScaleVolumeUpper, OAI.RegularPointCoordinates.patchLocalizationFactor