OAI/GroupTheory/PolycyclicRecognition/Algebra/PositiveWidthAbsorption.lean
4 declarations, 0 contain sorry, 0 declared as axioms
Absorption of small exponential errors by positive ideal widths
- theorem
OAI.PolycyclicRecognition.positive_width_coordinate_boundline 17Source documentation
Positive coordinate widths give a uniform exponential gain, without any norm on the abstract Lie algebra.
theorem positive_width_coordinate_bound (b : Basis J ℝ V) (cost : J → ℝ) {lo r : ℝ} (hlo : ∀ j, lo ≤ cost j) (hr : 0 ≤ r) (v : V) : ‖(exponentialRescaleBasis b cost r).equivFun v‖ ≤ Real.exp (-lo * r) * ‖b.equivFun v‖ := by … - theorem
OAI.PolycyclicRecognition.eventually_positive_width_absorbsline 32Source documentation
The strict gap absorbs the entire error ball, uniformly over its points. This is the final small-error step for the ideal coordinate of a lift.
theorem eventually_positive_width_absorbs (b : Basis J ℝ V) (cost : J → ℝ) {lo α : ℝ} (hlo : ∀ j, lo ≤ cost j) (hgap : α < lo) (ε : ℝ → ℝ) (hε : Tendsto ε atTop (𝓝 0)) : ∀ᶠ r in atTop, ∀ v : V, ‖b.equivFun v‖ ≤ Real.exp ((α + ε r) * r) → ‖(exponentialRescaleBasis b cost r).equivFun v‖ ≤ 1 := by … - theorem
OAI.PolycyclicRecognition.exists_positive_width_absorption_thresholdline 50Source documentation
A single explicit positive threshold works for every allowed error sequence and every point satisfying its logarithmic bound.
theorem exists_positive_width_absorption_threshold (b : Basis J ℝ V) (cost : J → ℝ) {lo U : ℝ} (hlo : 0 < lo) (hcost : ∀ j, lo ≤ cost j) (hU : 0 < U) : ∃ δ₀ : ℝ, 0 < δ₀ ∧ ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ → ∀ ε : ℝ → ℝ, Tendsto ε atTop (𝓝 0) → ∀ᶠ r in atTop, ∀ v : V, ‖b.equivFun v‖ ≤ Real.exp ((U * δ + ε r) * r) → ‖(exponentialRescaleBasis b cost r).equivFun v‖ ≤ 1 := by … - theorem
OAI.PolycyclicRecognition.eventually_positive_width_absorbs_polynomialline 68Source documentation
A fixed polynomial in a small exponential error is still absorbed by positive widths. The threshold depends on the polynomial degree.
theorem eventually_positive_width_absorbs_polynomial (b : Basis J ℝ V) (cost : J → ℝ) {lo α K : ℝ} (p : ℕ) (hcost : ∀ j, lo ≤ cost j) (hK : 0 ≤ K) (hα : 0 ≤ α) (hgap : (p : ℝ) * α < lo) (ε : ℝ → ℝ) (hε : Tendsto ε atTop (𝓝 0)) : ∀ᶠ r in atTop, ∀ v : V, ‖b.equivFun v‖ ≤ K * (1 + Real.exp ((α + ε r) * r)) ^ p → ‖(exponentialRescaleBasis b cost r).equivFun v‖ ≤ 1 := by …