ScaleLabelStabilization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Passing from adjacent-scale comparisons to uniform stabilization

theorem OAI.PolycyclicRecognition.scale_label_eq_of_nearby line 14

Source documentation

Nearby-scale equality propagates along a finite geometric chain.

theorem scale_label_eq_of_nearby
    {P L : Type*} (label : P → ℝ → L) {q R : ℝ} (hq : 1 < q) (hR : 0 < R)
    (hnear : ∀ p r t, R ≤ r → r ≤ t → t ≤ q * r → label p r = label p t) :
    ∀ p r, R ≤ r → label p r = label p R := by
…

theorem OAI.PolycyclicRecognition.uniform_nearby_bound_of_strict_sequences line 45

Source documentation

Sequential comparison at arbitrary increasing source and target scales is enough for the uniform estimate used in the geometric telescoping step.

theorem uniform_nearby_bound_of_strict_sequences
    {P : Type*} (err : P → ℝ → ℝ → ℝ) (q : ℝ)
    (hseq : ∀ (p : ℕ → P) (r t : ℕ → ℝ),
      Tendsto r atTop atTop → StrictMono r → StrictMono t →
      (∀ n, 1 ≤ r n) → (∀ n, r n ≤ t n) → (∀ n, t n ≤ q * r n) →
      Tendsto (fun n => err (p n) (r n) (t n)) atTop (𝓝 0)) :
    ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, 1 ≤ R ∧
      ∀ p r t, R ≤ r → r ≤ t → t ≤ q * r → err p r t ≤ ε := by
…

theorem OAI.PolycyclicRecognition.uniform_nearby_labels_of_strict_sequences line 74

Source documentation

Eventual equality along every scale sequence yields a single uniform threshold for all maps and basepoints.

theorem uniform_nearby_labels_of_strict_sequences
    {P L : Type*} (label : P → ℝ → L) (q : ℝ)
    (hseq : ∀ (p : ℕ → P) (r t : ℕ → ℝ),
      Tendsto r atTop atTop → StrictMono r → StrictMono t →
      (∀ n, 1 ≤ r n) → (∀ n, r n ≤ t n) → (∀ n, t n ≤ q * r n) →
      ∀ᶠ n in atTop, label (p n) (r n) = label (p n) (t n)) :
    ∃ R : ℝ, 1 ≤ R ∧ ∀ p r t, R ≤ r → r ≤ t → t ≤ q * r →
      label p r = label p t := by
…

theorem OAI.PolycyclicRecognition.physical_offset_increment_eq line 97

theorem OAI.PolycyclicRecognition.uniform_zero_of_normalized_scale_increments line 108

Source documentation

The normalized mean offsets vanish uniformly once their comparisons at nearby scales vanish uniformly.

theorem uniform_zero_of_normalized_scale_increments
    {P W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (b : P → ℝ → W) {Q C : ℝ} (hQ : 1 < Q)
    (hbound : ∀ p r, 1 ≤ r → ‖b p r‖ ≤ C)
    (hnear : ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, 1 ≤ R ∧
      ∀ p r t, R ≤ r → r ≤ t → t ≤ Q * r →
        dist (b p r) ((t / r) • b p t) ≤ ε) :
    ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, 1 ≤ R ∧
      ∀ p r, R ≤ r → ‖b p r‖ ≤ ε := by
…

theorem OAI.PolycyclicRecognition.uniform_scale_stabilization_of_sequences line 157

Source documentation

The two conclusions needed from adjacent-scale comparison: a uniform stable label and a uniformly vanishing normalized offset.

theorem uniform_scale_stabilization_of_sequences
    {P L W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (label : P → ℝ → L) (b : P → ℝ → W) {Q C : ℝ} (hQ : 1 < Q)
    (hbound : ∀ p r, 1 ≤ r → ‖b p r‖ ≤ C)
    (hseq : ∀ (p : ℕ → P) (r t : ℕ → ℝ),
      Tendsto r atTop atTop → StrictMono r → StrictMono t →
      (∀ n, 1 ≤ r n) → (∀ n, r n ≤ t n) → (∀ n, t n ≤ Q * r n) →
      (∀ᶠ n in atTop, label (p n) (r n) = label (p n) (t n)) ∧
      Tendsto (fun n => dist (b (p n) (r n)) ((t n / r n) • b (p n) (t n)))
        atTop (𝓝 0)) :
    (∃ R : ℝ, 1 ≤ R ∧ ∀ p r, R ≤ r → label p r = label p R) ∧
    (∀ ε : ℝ, 0 < ε → ∃ R : ℝ, 1 ≤ R ∧ ∀ p r, R ≤ r → ‖b p r‖ ≤ ε) := by
…