OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanOffsetThreshold.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_source_offset_threshold line 14

   Source documentation

   The source enlargement and the vanishing-rate tolerance are chosen from the fixed metric constants and target restriction threshold. Neither depends on the source section, the sample, or the path-length constant.

   theorem exists_source_offset_threshold
       {A B Λ c target source : ℝ}
       (hA : 0 ≤ A) (hB : 0 ≤ B) (hΛ : 0 ≤ Λ) (hc : 0 ≤ c)
       (htarget : 0 < target) (hsource : 0 < source) :
       ∃ δ₀ ε : ℝ, 0 < δ₀ ∧ 0 < ε ∧ δ₀ ≤ source ∧
         ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
           c * δ ≤ 1 ∧ Λ * (A * δ + B * ε) ≤ target := by
   …

2. theorem OAI.PolycyclicRecognition.exists_uniform_source_offset_threshold line 48

   Source documentation

   A single source enlargement works for the finite family of possible affine labels and cone tests. The family is fixed before taking a limiting neighboring law.

   theorem exists_uniform_source_offset_threshold
       {I : Type*} [Finite I] [Nonempty I]
       {A B Λ c source : ℝ} (target : I → ℝ)
       (hA : 0 ≤ A) (hB : 0 ≤ B) (hΛ : 0 ≤ Λ) (hc : 0 ≤ c)
       (htarget : ∀ i, 0 < target i) (hsource : 0 < source) :
       ∃ δ₀ ε : ℝ, 0 < δ₀ ∧ 0 < ε ∧ δ₀ ≤ source ∧
         ∀ (i : I) (δ : ℝ), 0 < δ → δ ≤ δ₀ →
           c * δ ≤ 1 ∧ Λ * (A * δ + B * ε) ≤ target i := by
   …