Abstract-real scale lemmas for the separated-chains argument

Pure real algebra (no stream sequences): the choice of the cosine mode in a window [E^s, c₁ E^{s-d}], the exponent bookkeeping λ E^{2s} ≤ 1, E^{2d} ≤ c₁² λ E^{2s}, the passage from a log-ratio near log 4 to a ratio in [3,5], the geometric sum, and the decay of the scales ε_m → 0.

theorem AVenhance.Infra.FullTheorem.NoSel.exists_big (C θ ρ : ℝ) (hρ : 0 < ρ) (hθ : 0 < θ) : ∃ (Λ₀ : ℝ), ∀ (x : ℝ), Λ₀ ≤ x → C * x⁻¹ ^ ρ ≤ θ

C (x⁻¹)^ρ ≤ θ for all large x.

theorem AVenhance.Infra.FullTheorem.NoSel.mul_rpow_le_inv {C ε x ρ : ℝ} (hC : 0 ≤ C) (hε : 0 ≤ ε) (hεx : ε ≤ x⁻¹) (hρ : 0 ≤ ρ) : C * ε ^ ρ ≤ C * x⁻¹ ^ ρ

Monotonicity used to pass from ε ≤ x⁻¹ to the smallness condition.

theorem AVenhance.Infra.FullTheorem.NoSel.exists_mode {c₁ E s d : ℝ} (hc₁ : 0 < c₁) (hE : 0 < E) (hE2 : 2 * E ^ d ≤ c₁) (hX : 2 * Real.pi * (c₁ * E ^ (s - d)) ≤ 1 / 2) : ∃ (n : ℕ), 1 ≤ n ∧ E ^ s ≤ 1 / (2 * Real.pi * ↑n) ∧ 1 / (2 * Real.pi * ↑n) ≤ c₁ * E ^ (s - d) ∧ 1 / (2 * Real.pi * (c₁ * E ^ (s - d))) ≤ ↑n

A cosine mode n with L_n := 1/(2πn) in the window [E^s, c₁ E^{s-d}], and n large.

theorem AVenhance.Infra.FullTheorem.NoSel.scale_algebra {E L lam c₁ s d : ℝ} (hE : 0 < E) (hL : 0 < L) (hlam : lam * L ^ 2 = 1) (hlo : E ^ s ≤ L) (hup : L ≤ c₁ * E ^ (s - d)) : lam * E ^ (2 * s) ≤ 1 ∧ E ^ (2 * d) ≤ c₁ ^ 2 * (lam * E ^ (2 * s))

Exponent bookkeeping for the cosine window.

theorem AVenhance.Infra.FullTheorem.NoSel.ratio_of_log {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (h : |Real.log (b / a) - Real.log 4| ≤ Real.log (5 / 4)) : 3 * a ≤ b ∧ b ≤ 5 * a

A log-ratio within log (5/4) of log 4 forces the ratio into [3,5].

theorem AVenhance.Infra.FullTheorem.NoSel.ratio_of_log' {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (h : |Real.log (b / a) + Real.log 4| ≤ Real.log (5 / 4)) : 3 * b ≤ a ∧ a ≤ 5 * b

Reverse ratio: |log (b/a) + log 4| ≤ log (5/4) gives 3 b ≤ a ≤ 5 b.

theorem AVenhance.Infra.FullTheorem.NoSel.final_ineq {a b v₁ v₂ u₁ u₂ G τ e : ℝ} (h1 : |a - v₁| ≤ τ) (h2 : |b - v₂| ≤ τ) (h3 : |v₁ - u₁| ≤ e) (h4 : |v₂ - u₂| ≤ e) (hG : G ≤ |u₁ - u₂|) : G - 2 * τ - 2 * e ≤ |a - b|

Triangle bookkeeping of the final comparison.

theorem AVenhance.Infra.FullTheorem.NoSel.geom_sum_le {a : ℕ → ℝ} {n₀ : ℕ} (hr : ∀ (k : ℕ), n₀ ≤ k → a (k + 1) ≤ a k / 2) (M : ℕ) (hM : n₀ ≤ M) : ∑ l ∈ Finset.Ioc n₀ M, a (l - 1) ≤ 2 * a n₀ - 2 * a M

Geometric sum ∑_{l ∈ (n₀, M]} a (l-1) ≤ 2 a n₀.

theorem AVenhance.Infra.FullTheorem.NoSel.epsilon_tendsto {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : Filter.Tendsto (fun (m : ℕ) => epsilon β Λ m) Filter.atTop (nhds 0)

ε_m → 0.

theorem AVenhance.Infra.FullTheorem.NoSel.epsilon_rpow_eventually {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {a X : ℝ} (K : ℝ) (ha : 0 < a) (hX : 0 < X) : ∃ (J : ℕ), ∀ (M : ℕ), J ≤ M → K * epsilon β Λ M ^ a ≤ X

K ε_M^a ≤ X for all large M.

theorem AVenhance.Infra.FullTheorem.NoSel.epsilon_exists_small {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {e X : ℝ} (c₁ : ℝ) (he : 0 < e) (hX : 0 < X) (N₀ : ℕ) : ∃ (m : ℕ), N₀ ≤ m ∧ c₁ * epsilon β Λ m ^ e < X

Some large level has c₁ ε_m^e small.