Choosing step counts in Archimedean ordered semifields

This file chooses a positive number of steps n with L * n⁻¹ < c, which splits a segment into n steps of length n⁻¹ with an error of at most c.

It also chooses the length of a finite geometric sequence of exponents. Given a ratio r > 1 and a target s < r, it finds a number M ≥ 1 of steps such that the starting value s / r ^ M lies below any prescribed p > 0 while every term s / r ^ M * r ^ k with k < M stays below 1. Moser's iteration uses it to pick the exponents p₀ χ^k along which a reverse Hölder inequality is iterated.

Main results

• TauCeti.exists_pos_nat_mul_inv_lt: for 0 < c there is n > 0 with L * n⁻¹ < c.
• TauCeti.exists_div_pow_lt_and_forall_mul_pow_lt_one: for 1 < r, s < r and 0 < p there is M > 0 with s / r ^ M < p and s / r ^ M * r ^ k < 1 for all k < M.
• TauCeti.exists_nat_ge_and_div_le: for 0 < δ and n₀ : ℕ there are n ≥ n₀ and N > 0 with 1 / (N + 1) ≤ δ and 2 * n / N ≤ δ.

theorem TauCeti.exists_div_pow_lt_and_forall_mul_pow_lt_one {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] [ExistsAddOfLE K] {r s p : K} (hr : 1 < r) (hsr : s < r) (hp : 0 < p) : ∃ (M : ℕ), 0 < M ∧ s / r ^ M < p ∧ ∀ k < M, s / r ^ M * r ^ k < 1

For r > 1, s < r and p > 0 there is a number M ≥ 1 of steps such that the starting value s / r ^ M is below p, and the terms s / r ^ M * r ^ k of the geometric sequence for the steps k < M stay below 1.

theorem TauCeti.exists_pos_nat_mul_inv_lt {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] (L : K) {c : K} (hc : 0 < c) : ∃ (n : ℕ), 0 < n ∧ L * (↑n)⁻¹ < c

For any L and c > 0 there is a positive integer n with L * n⁻¹ < c.

theorem TauCeti.exists_nat_ge_and_div_le {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {δ : K} (hδ : 0 < δ) (n₀ : ℕ) : ∃ (n : ℕ) (N : ℕ), 0 < n ∧ n₀ ≤ n ∧ 0 < N ∧ 1 / (↑N + 1) ≤ δ ∧ 2 * ↑n / ↑N ≤ δ

For δ > 0 and any n₀, there are a positive n ≥ n₀ and a positive N so large that both 1 / (N + 1) and 2 * n / N are at most δ.