PatchLocalization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Localization of active coordinate patches

A cutoff support bounds the finely normalized displacement. Coarse harmonic separation and sublinear growth of the normalizations then bound the original metric distance. The squared growth hypothesis below is the exponent-one bound for squared norms (equivalently, exponent one-half for norms).

theorem OAI.RegularPointCoordinates.normalized_cutoff_support_norm_le line 31

Source documentation

Membership in the actual topological support of a normalized cutoff bounds its normalized displacement, including boundary support points.

theorem normalized_cutoff_support_norm_le (T : E →L[ℝ] F) (c x : E)
    (psi : F → ℝ) {r L : ℝ} (hr : 0 < r)
    (hsupport : tsupport psi ⊆ Metric.closedBall 0 L)
    (hx : x ∈ tsupport (fun P => psi (r⁻¹ • T (P - c)))) :
    ‖T (x - c)‖ ≤ L * r := by
…

theorem OAI.RegularPointCoordinates.distance_le_of_normalization_growth line 48

Source documentation

A coarse lower bound and sublinear normalization growth localize a fine-scale displacement. The estimate is uniform in the scale r.

theorem distance_le_of_normalization_growth {d r c M L A B : ℝ}
    (hd : 0 ≤ d) (hr : 0 < r) (hc : 0 < c) (hL : 0 ≤ L)
    (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hsmall : A ≤ L * r) (hseparate : c * d ≤ B)
    (hgrowth : B ^ 2 ≤ M ^ 2 * (d / r) * A ^ 2) :
    d ≤ (M * L / c) ^ 2 * r := by
…

theorem OAI.RegularPointCoordinates.squared_growth_of_slow_norm_growth line 81

Source documentation

Any slow norm-growth exponent at most one-half gives the squared growth bound used in localization, at all coarser scales.

theorem squared_growth_of_slow_norm_growth (T S : E →L[ℝ] F) (w : E)
    {d r M a : ℝ} (hr : 0 < r) (hdr : r ≤ d) (hM : 0 ≤ M) (ha : a ≤ 1 / 2)
    (hslow : ‖S w‖ ≤ M * (d / r) ^ a * ‖T w‖) :
    ‖S w‖ ^ 2 ≤ M ^ 2 * (d / r) * ‖T w‖ ^ 2 := by
…

theorem OAI.RegularPointCoordinates.active_cutoff_distance_le line 102

Source documentation

Active support forces an original-metric distance bound. Separation and comparison are only required when the distance exceeds the fine scale, so nearby pairs need no coarse-scale selection.

theorem active_cutoff_distance_le (u : X → E) (T S : E →L[ℝ] F)
    (psi : F → ℝ) (x y : X) {r c M L : ℝ}
    (hr : 0 < r) (hc : 0 < c) (hL : 0 ≤ L)
    (hsupport : tsupport psi ⊆ Metric.closedBall 0 L)
    (hactive : u x ∈ tsupport (fun P => psi (r⁻¹ • T (P - u y))))
    (hseparate : r < dist x y → c * dist x y ≤ ‖S (u x - u y)‖)
    (hgrowth : r < dist x y →
      ‖S (u x - u y)‖ ^ 2 ≤ M ^ 2 * (dist x y / r) * ‖T (u x - u y)‖ ^ 2) :
    dist x y ≤ max 1 ((M * L / c) ^ 2) * r := by
…

theorem OAI.RegularPointCoordinates.active_cutoff_distance_le_of_slow_growth line 123

Source documentation

The same localization, stated directly with the manuscript's slow power growth instead of its squared consequence.

theorem active_cutoff_distance_le_of_slow_growth (u : X → E) (T S : E →L[ℝ] F)
    (psi : F → ℝ) (x y : X) {r c M L a : ℝ}
    (hr : 0 < r) (hc : 0 < c) (hM : 0 ≤ M) (hL : 0 ≤ L) (ha : a ≤ 1 / 2)
    (hsupport : tsupport psi ⊆ Metric.closedBall 0 L)
    (hactive : u x ∈ tsupport (fun P => psi (r⁻¹ • T (P - u y))))
    (hseparate : r < dist x y → c * dist x y ≤ ‖S (u x - u y)‖)
    (hslow : r < dist x y →
      ‖S (u x - u y)‖ ≤ M * (dist x y / r) ^ a * ‖T (u x - u y)‖) :
    dist x y ≤ max 1 ((M * L / c) ^ 2) * r := by
…

theorem OAI.RegularPointCoordinates.normalized_cutoff_eq_one_of_norm_le line 137

Source documentation

The cutoff equals one on the fine normalized core.

theorem normalized_cutoff_eq_one_of_norm_le (T : E →L[ℝ] F) (psi : F → ℝ)
    (c P : E) {r L : ℝ} (hr : 0 < r)
    (hcore : ∀ v, ‖v‖ ≤ L → psi v = 1)
    (hnorm : ‖T (P - c)‖ ≤ L * r) :
    psi (r⁻¹ • T (P - c)) = 1 := by
…

theorem OAI.RegularPointCoordinates.exists_weight_one_covering_patch line 152

Source documentation

Net covering produces an active weight-one patch. Its enlarged source ball covers the testing ball, exactly as required for the lower cumulative mass comparison.

theorem exists_weight_one_covering_patch (A : Set X) (hA : TotallyBounded A)
    (r : ℝ≥0) (hr : 0 < r) (u : X → E) (T : X → E →L[ℝ] F)
    (psi : F → ℝ) (hcore : ∀ v, ‖v‖ ≤ 2 → psi v = 1)
    (hnear : ∀ x ∈ A, ∀ y ∈ maximalPatchNet r A, dist x y ≤ r →
      ‖T y (u x - u y)‖ ≤ 2 * r)
    (x : X) (hx : x ∈ A) {L : ℝ} (hL : 2 ≤ L) :
    ∃ y ∈ maximalPatchNet r A,
      dist x y ≤ r ∧ psi ((r : ℝ)⁻¹ • T y (u x - u y)) = 1 ∧
      u x ∈ tsupport (fun P => psi ((r : ℝ)⁻¹ • T y (P - u y))) ∧
      Metric.ball x r ⊆ Metric.ball y (L * r) := by
…

Mentions: OAI.RegularPointCoordinates.maximalPatchNet

theorem OAI.RegularPointCoordinates.active_normalized_cutoff_card_le line 182

Source documentation

The overlap bound for the actual normalized cutoffs: active-center distance is derived from support, harmonic separation, and normalization growth before the disjoint-ball volume count is applied.

theorem active_normalized_cutoff_card_le (μ : Measure X) (A : Set X)
    (r : ℝ≥0) (u : X → E) (T S : X → E →L[ℝ] F) (psi : F → ℝ)
    (x : X) (n : ℕ) (hr : 0 < r) {c M L a b : ℝ}
    (hc : 0 < c) (hL : 0 ≤ L) (ha : 0 < a)
    (hsupport : tsupport psi ⊆ Metric.closedBall 0 L)
    (hseparate : ∀ y ∈ maximalPatchNet r A, (r : ℝ) < dist x y →
      c * dist x y ≤ ‖S y (u x - u y)‖)
    (hgrowth : ∀ y ∈ maximalPatchNet r A, (r : ℝ) < dist x y →
      ‖S y (u x - u y)‖ ^ 2 ≤ M ^ 2 * (dist x y / r) * ‖T y (u x - u y)‖ ^ 2)
    (hlower : ∀ y ∈ maximalPatchNet r A,
      a * ((r : ℝ) / 2) ^ n ≤ μ.real (Metric.ball y (r / 2)))
    (hupper : μ.real (Metric.ball x (max 1 ((M * L / c) ^ 2) * r + r / 2)) ≤
…

Mentions: OAI.RegularPointCoordinates.maximalPatchNet