BoundaryLimits.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Limits of contracting boundary trajectories

Polynomial times exponential decay is summable. Metric trajectories with a common increment bound converge uniformly, with a common tail bound and compact normalized shadow. Asymptotic representatives of a quotient point have equal limits and determine a continuous boundary map.

theorem OAI.PolycyclicRecognition.summable_polynomial_exp_decay line 25

Source documentation

The summable increment profile appearing in the ray-boundary proof.

theorem summable_polynomial_exp_decay (C : ℝ) (M : ℕ) {c : ℝ} (hc : 0 < c) :
    Summable (fun n : ℕ => C * (1 + (n : ℝ)) ^ M * Real.exp (-c * n)) := by
…

theorem OAI.PolycyclicRecognition.exists_uniform_limit_of_summable_steps line 48

Source documentation

A common summable increment bound gives actual limits, a common tail estimate, and uniform convergence of the family of trajectories.

theorem exists_uniform_limit_of_summable_steps
    (f : P → ℕ → Y) (d : ℕ → ℝ) (hd : Summable d)
    (hstep : ∀ p n, dist (f p n) (f p (n + 1)) ≤ d n) :
    ∃ b : P → Y,
      (∀ p, Tendsto (f p) atTop (𝓝 (b p))) ∧
      (∀ p n, dist (f p n) (b p) ≤ ∑' k, d (n + k)) ∧
      TendstoUniformly (fun n p => f p n) b atTop := by
…

theorem OAI.PolycyclicRecognition.boundary_limits_eq_of_asymptotic line 68

Source documentation

Asymptotic trajectories represent the same boundary point.

theorem boundary_limits_eq_of_asymptotic
    (f g : ℕ → Y) {a b : Y}
    (hf : Tendsto f atTop (𝓝 a)) (hg : Tendsto g atTop (𝓝 b))
    (hfg : Tendsto (fun n => dist (f n) (g n)) atTop (𝓝 0)) : a = b := by
…

theorem OAI.PolycyclicRecognition.exists_continuous_quotient_boundary line 77

Source documentation

Uniform trajectory convergence and asymptotic equality on quotient fibers construct the continuous boundary map. The displayed tail estimate is independent of the quotient point and representative.

theorem exists_continuous_quotient_boundary
    [TopologicalSpace P] [TopologicalSpace Q]
    (q : P → Q) (hq : Topology.IsQuotientMap q)
    (f : P → ℕ → Y) (hcont : ∀ n, Continuous (fun p => f p n))
    (d : ℕ → ℝ) (hd : Summable d)
    (hstep : ∀ p n, dist (f p n) (f p (n + 1)) ≤ d n)
    (hfiber : ∀ p p', q p = q p' →
      Tendsto (fun n => dist (f p n) (f p' n)) atTop (𝓝 0)) :
    ∃ b : Q → Y, Continuous b ∧
      TendstoUniformly (fun n p => f p n) (fun p => b (q p)) atTop ∧
      ∀ p n, dist (f p n) (b (q p)) ≤ ∑' k, d (n + k) := by
…

theorem OAI.PolycyclicRecognition.exists_compact_boundary_shadow line 105

Source documentation

In the polynomial-exponential case the normalized limit lies in one fixed compact ball, uniformly over all initial trajectories.

theorem exists_compact_boundary_shadow [ProperSpace Y]
    (f : P → ℕ → Y) (y₀ : Y) (hstart : ∀ p, f p 0 = y₀)
    (C : ℝ) (M : ℕ) {c : ℝ} (hc : 0 < c)
    (hstep : ∀ p n, dist (f p n) (f p (n + 1)) ≤
      C * (1 + (n : ℝ)) ^ M * Real.exp (-c * n)) :
    ∃ (K : Set Y) (b : P → Y), IsCompact K ∧
      (∀ p, Tendsto (f p) atTop (𝓝 (b p))) ∧ (∀ p, b p ∈ K) := by
…