English
For LiouvilleWith p x, subtracting an integer m preserves the LiouvilleWith property: LiouvilleWith p (x − m) ⇔ LiouvilleWith p x.
Русский
Свойство LiouvilleWith сохраняется при вычитании целого числа: LiouvilleWith p (x − m) ⇔ LiouvilleWith p x.
LaTeX
$$@[simp] theorem sub_int_iff : LiouvilleWith p (x - m.cast) ↔ LiouvilleWith p x$$
Lean4
/-- Let `Z, N` be types, let `R` be a metric space, let `α : R` be a point and let
`j : Z → N → R` be a function. We aim to estimate how close we can get to `α`, while staying
in the image of `j`. The points `j z a` of `R` in the image of `j` come with a "cost" equal to
`d a`. As we get closer to `α` while staying in the image of `j`, we are interested in bounding
the quantity `d a * dist α (j z a)` from below by a strictly positive amount `1 / A`: the intuition
is that approximating well `α` with the points in the image of `j` should come at a high cost. The
hypotheses on the function `f : R → R` provide us with sufficient conditions to ensure our goal.
The first hypothesis is that `f` is Lipschitz at `α`: this yields a bound on the distance.
The second hypothesis is specific to the Liouville argument and provides the missing bound
involving the cost function `d`.
This lemma collects the properties used in the proof of `exists_pos_real_of_irrational_root`.
It is stated in more general form than needed: in the intended application, `Z = ℤ`, `N = ℕ`,
`R = ℝ`, `d a = (a + 1) ^ f.nat_degree`, `j z a = z / (a + 1)`, `f ∈ ℤ[x]`, `α` is an irrational
root of `f`, `ε` is small, `M` is a bound on the Lipschitz constant of `f` near `α`, `n` is
the degree of the polynomial `f`.
-/
theorem exists_one_le_pow_mul_dist {Z N R : Type*} [PseudoMetricSpace R] {d : N → ℝ} {j : Z → N → R} {f : R → R} {α : R}
{ε M : ℝ}
-- denominators are positive
(d0 : ∀ a : N, 1 ≤ d a)
(e0 : 0 < ε)
-- function is Lipschitz at α
(B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M)
-- clear denominators
(L : ∀ ⦃z : Z⦄, ∀ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))) :
∃ A : ℝ, 0 < A ∧ ∀ z : Z, ∀ a : N, 1 ≤ d a * (dist α (j z a) * A) := by
-- A useful inequality to keep at hand
have me0 : 0 < max (1 / ε) M :=
lt_max_iff.mpr
(Or.inl (one_div_pos.mpr e0))
-- The maximum between `1 / ε` and `M` works
refine
⟨max (1 / ε) M, me0, fun z a => ?_⟩
-- First, let's deal with the easy case in which we are far away from `α`
by_cases dm1 : 1 ≤ dist α (j z a) * max (1 / ε) M
· exact one_le_mul_of_one_le_of_one_le (d0 a) dm1
· -- `j z a = z / (a + 1)`: we prove that this ratio is close to `α`
have : j z a ∈ closedBall α ε :=
by
refine mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))
exact (le_div_iff₀ me0).mpr (not_le.mp dm1).le
refine
(L this).trans
?_
-- remove a common factor and use the Lipschitz assumption `B`
gcongr
· exact zero_le_one.trans (d0 a)
· refine (B this).trans ?_
gcongr
apply le_max_right
