OAI/Geometry/RCD/Harmonic/ProjectionFailureSequence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.projection_failure_sequence_with_ratio_bound line 18

   Source documentation

   Failure of every uniform late-space bound gives increasingly Euclidean configurations whose source error is negligible relative to the residual. Positivity of the source floor guarantees valid division.

   theorem projection_failure_sequence_with_ratio_bound {I : Type*} (epsilon residual source : I → ℝ)
       (hε : ∀ i, 0 ≤ epsilon i) (hs : ∀ i, 0 < source i)
       (hfail : ¬∃ C : ℝ, 0 < C ∧ ∃ δ : ℝ, 0 < δ ∧
         ∀ i, epsilon i < δ → residual i ≤ C * source i) :
       ∃ q : ℕ → I, (∀ j, 0 < residual (q j)) ∧
         Tendsto (epsilon ∘ q) atTop (𝓝 0) ∧
         Tendsto (fun j => source (q j) / residual (q j)) atTop (𝓝 0) ∧
         (∀ j, source (q j) / residual (q j) ≤ 1) := by
   …

2. theorem OAI.RegularPointCoordinates.projection_failure_sequence line 47

   Source documentation

   The failure sequence without the additional pointwise ratio bound.

   theorem projection_failure_sequence {I : Type*} (epsilon residual source : I → ℝ)
       (hε : ∀ i, 0 ≤ epsilon i) (hs : ∀ i, 0 < source i)
       (hfail : ¬∃ C : ℝ, 0 < C ∧ ∃ δ : ℝ, 0 < δ ∧
         ∀ i, epsilon i < δ → residual i ≤ C * source i) :
       ∃ q : ℕ → I, (∀ j, 0 < residual (q j)) ∧
         Tendsto (epsilon ∘ q) atTop (𝓝 0) ∧
         Tendsto (fun j => source (q j) / residual (q j)) atTop (𝓝 0) := by
   …