feat: FloorSemiring.tendsto_pow_div_factorial (#17119)

#12191 added some technical lemmas for #6718, but eventually they were not needed. This PR deprecates them and adds generalized lemmas.

Author: astrainfinita

Mathlib.lean

@@ -3613,6 +3613,7 @@ import Mathlib.Order.Filter.AtTopBot
 import Mathlib.Order.Filter.AtTopBot.Archimedean
 import Mathlib.Order.Filter.AtTopBot.BigOperators
 import Mathlib.Order.Filter.AtTopBot.Field
+import Mathlib.Order.Filter.AtTopBot.Floor
 import Mathlib.Order.Filter.AtTopBot.Group
 import Mathlib.Order.Filter.AtTopBot.ModEq
 import Mathlib.Order.Filter.AtTopBot.Monoid

Mathlib/Algebra/Order/Floor/Prime.lean

@@ -3,40 +3,44 @@ Copyright (c) 2022 Yuyang Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuyang Zhao
 -/
-
-import Mathlib.Algebra.Order.Floor
 import Mathlib.Data.Nat.Prime.Basic
+import Mathlib.Topology.Algebra.Order.Floor
 
 /-!
 # Existence of a sufficiently large prime for which `a * c ^ p / (p - 1)! < 1`
 
 This is a technical result used in the proof of the Lindemann-Weierstrass theorem.
--/
 
-namespace FloorRing
+TODO: delete this file, as all its lemmas have been deprecated.
+-/
 
 open scoped Nat
 
+@[deprecated eventually_mul_pow_lt_factorial_sub (since := "2024-09-25")]
+theorem Nat.exists_prime_mul_pow_lt_factorial (n a c : ℕ) :
+    ∃ p > n, p.Prime ∧ a * c ^ p < (p - 1)! :=
+  ((Filter.frequently_atTop.mpr Nat.exists_infinite_primes).and_eventually
+    (eventually_mul_pow_lt_factorial_sub a c 1)).forall_exists_of_atTop (n + 1)
+
+namespace FloorRing
+
 variable {K : Type*}
 
+@[deprecated FloorSemiring.eventually_mul_pow_lt_factorial_sub (since := "2024-09-25")]
 theorem exists_prime_mul_pow_lt_factorial [LinearOrderedRing K] [FloorRing K] (n : ℕ) (a c : K) :
-    ∃ p > n, p.Prime ∧ a * c ^ p < (p - 1)! := by
-  obtain ⟨p, pn, pp, h⟩ := n.exists_prime_mul_pow_lt_factorial ⌈|a|⌉.natAbs ⌈|c|⌉.natAbs
-  use p, pn, pp
-  calc a * c ^ p
-    _ ≤ |a * c ^ p| := le_abs_self _
-    _ ≤ ⌈|a|⌉ * (⌈|c|⌉ : K) ^ p := ?_
-    _ = ↑(Int.natAbs ⌈|a|⌉ * Int.natAbs ⌈|c|⌉ ^ p) := ?_
-    _ < ↑(p - 1)! := Nat.cast_lt.mpr h
-  · rw [abs_mul, abs_pow]
-    gcongr <;> try first | positivity | apply Int.le_ceil
-  · simp_rw [Nat.cast_mul, Nat.cast_pow, Int.cast_natAbs,
-      abs_eq_self.mpr (Int.ceil_nonneg (abs_nonneg (_ : K)))]
+    ∃ p > n, p.Prime ∧ a * c ^ p < (p - 1)! :=
+  ((Filter.frequently_atTop.mpr Nat.exists_infinite_primes).and_eventually
+    (FloorSemiring.eventually_mul_pow_lt_factorial_sub a c 1)).forall_exists_of_atTop (n + 1)
 
+@[deprecated FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop (since := "2024-09-25")]
 theorem exists_prime_mul_pow_div_factorial_lt_one [LinearOrderedField K] [FloorRing K]
     (n : ℕ) (a c : K) :
-    ∃ p > n, p.Prime ∧ a * c ^ p / (p - 1)! < 1 := by
-  simp_rw [div_lt_one (α := K) (Nat.cast_pos.mpr (Nat.factorial_pos _))]
-  exact exists_prime_mul_pow_lt_factorial ..
+    ∃ p > n, p.Prime ∧ a * c ^ p / (p - 1)! < 1 :=
+  letI := Preorder.topology K
+  haveI : OrderTopology K := ⟨rfl⟩
+  ((Filter.frequently_atTop.mpr Nat.exists_infinite_primes).and_eventually
+    (eventually_lt_of_tendsto_lt zero_lt_one
+      (FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop a c 1))).forall_exists_of_atTop
+    (n + 1)
 
 end FloorRing

Mathlib/Analysis/ODE/PicardLindelof.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Winston Yin
 -/
 import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.Topology.Algebra.Order.Floor
 import Mathlib.Topology.MetricSpace.Contracting
 
 /-!
@@ -301,7 +302,7 @@ section
 
 theorem exists_contracting_iterate :
     ∃ (N : ℕ) (K : _), ContractingWith K (FunSpace.next : v.FunSpace → v.FunSpace)^[N] := by
-  rcases ((Real.tendsto_pow_div_factorial_atTop (v.L * v.tDist)).eventually
+  rcases ((FloorSemiring.tendsto_pow_div_factorial_atTop (v.L * v.tDist)).eventually
     (gt_mem_nhds zero_lt_one)).exists with ⟨N, hN⟩
   have : (0 : ℝ) ≤ (v.L * v.tDist) ^ N / N ! :=
     div_nonneg (pow_nonneg (mul_nonneg v.L.2 v.tDist_nonneg) _) (Nat.cast_nonneg _)

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -908,6 +908,8 @@ theorem Real.summable_pow_div_factorial (x : ℝ) : Summable (fun n ↦ x ^ n /
         norm_div, Real.norm_natCast, Nat.cast_succ]
     _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ := by gcongr
 
+@[deprecated "`Real.tendsto_pow_div_factorial_atTop` has been deprecated, use
+`FloorSemiring.tendsto_pow_div_factorial_atTop` instead" (since := "2024-10-05")]
 theorem Real.tendsto_pow_div_factorial_atTop (x : ℝ) :
     Tendsto (fun n ↦ x ^ n / n ! : ℕ → ℝ) atTop (𝓝 0) :=
   (Real.summable_pow_div_factorial x).tendsto_atTop_zero

Mathlib/Data/Nat/Prime/Basic.lean

@@ -287,37 +287,6 @@ lemma Prime.pow_inj {p q m n : ℕ} (hp : p.Prime) (hq : q.Prime)
     (Prime.dvd_of_dvd_pow hq <| h.symm ▸ dvd_pow_self q (succ_ne_zero n))
   exact ⟨H, succ_inj'.mp <| Nat.pow_right_injective hq.two_le (H ▸ h)⟩
 
-theorem exists_pow_lt_factorial (c : ℕ) : ∃ n0 > 1, ∀ n ≥ n0, c ^ n < (n - 1)! := by
-  refine ⟨2 * (c ^ 2 + 1), ?_, ?_⟩
-  · omega
-  intro n hn
-  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le hn
-  obtain (rfl | c0) := c.eq_zero_or_pos
-  · simp [Nat.factorial_pos]
-  refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d) c0)).trans_lt ?_
-  convert_to (c ^ 2) ^ (c ^ 2 + d + 1) < (c ^ 2 + (c ^ 2 + d + 1))!
-  · rw [← pow_mul, ← pow_add]
-    congr 1
-    omega
-  · congr
-    omega
-  refine lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial
-  rw [← one_mul (_ ^ _ : ℕ)]
-  exact Nat.mul_lt_mul_of_le_of_lt (Nat.one_le_of_lt (Nat.factorial_pos _))
-    (Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)) (Nat.factorial_pos _)
-
-theorem exists_mul_pow_lt_factorial (a : ℕ) (c : ℕ) : ∃ n0, ∀ n ≥ n0, a * c ^ n < (n - 1)! := by
-  obtain ⟨n0, hn, h⟩ := Nat.exists_pow_lt_factorial (a * c)
-  refine ⟨n0, fun n hn => lt_of_le_of_lt ?_ (h n hn)⟩
-  rw [mul_pow]
-  refine Nat.mul_le_mul_right _ (Nat.le_self_pow ?_ _)
-  omega
-
-theorem exists_prime_mul_pow_lt_factorial (n a c : ℕ) : ∃ p > n, p.Prime ∧ a * c ^ p < (p - 1)! :=
-  have ⟨n0, h⟩ := Nat.exists_mul_pow_lt_factorial a c
-  have ⟨p, hp, prime_p⟩ := (max (n + 1) n0).exists_infinite_primes
-  ⟨p, (le_max_left _ _).trans hp, prime_p, h _ <| le_of_max_le_right hp⟩
-
 end Nat
 
 namespace Int

Mathlib/Data/Real/Pi/Irrational.lean

@@ -5,6 +5,7 @@ Authors: Bhavik Mehta
 -/
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Data.Real.Irrational
+import Mathlib.Topology.Algebra.Order.Floor
 
 /-!
 # `Real.pi` is irrational
@@ -262,7 +263,7 @@ reformulation of tendsto_pow_div_factorial_atTop, which asserts the same for `a
 private lemma tendsto_pow_div_factorial_at_top_aux (a : ℝ) :
     Tendsto (fun n => (a : ℝ) ^ (2 * n + 1) / n !) atTop (nhds 0) := by
   rw [← mul_zero a]
-  refine ((tendsto_pow_div_factorial_atTop (a ^ 2)).const_mul a).congr (fun x => ?_)
+  refine ((FloorSemiring.tendsto_pow_div_factorial_atTop (a ^ 2)).const_mul a).congr (fun x => ?_)
   rw [← pow_mul, mul_div_assoc', _root_.pow_succ']
 
 /-- If `x` is rational, it can be written as `a / b` with `a : ℤ` and `b : ℕ` satisfying `b > 0`. -/

Mathlib/Order/Filter/AtTopBot.lean

@@ -1224,3 +1224,45 @@ theorem Antitone.piecewise_eventually_eq_iInter {β : α → Type*} [Preorder ι
   convert ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
   · convert congr_fun (Set.piecewise_compl (s _) g f) a
   · simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]
+
+namespace Nat
+
+theorem eventually_pow_lt_factorial_sub (c d : ℕ) : ∀ᶠ n in atTop, c ^ n < (n - d)! := by
+  rw [eventually_atTop]
+  refine ⟨2 * (c ^ 2 + d + 1), ?_⟩
+  intro n hn
+  obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le hn
+  obtain (rfl | c0) := c.eq_zero_or_pos
+  · simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]
+  refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_
+  convert_to (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
+  · rw [← pow_mul, ← pow_add]
+    congr 1
+    omega
+  · congr 1
+    omega
+  refine (lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <|
+    (factorial_le (Nat.le_succ _))
+  rw [← one_mul (_ ^ _ : ℕ)]
+  apply Nat.mul_lt_mul_of_le_of_lt
+  · exact Nat.one_le_of_lt (Nat.factorial_pos _)
+  · exact Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)
+  · exact (Nat.factorial_pos _)
+
+theorem eventually_mul_pow_lt_factorial_sub (a c d : ℕ) :
+    ∀ᶠ n in atTop, a * c ^ n < (n - d)! := by
+  filter_upwards [Nat.eventually_pow_lt_factorial_sub (a * c) d, Filter.eventually_gt_atTop 0]
+    with n hn hn0
+  rw [mul_pow] at hn
+  exact (Nat.mul_le_mul_right _ (Nat.le_self_pow hn0.ne' _)).trans_lt hn
+
+@[deprecated eventually_pow_lt_factorial_sub (since := "2024-09-25")]
+theorem exists_pow_lt_factorial (c : ℕ) : ∃ n0 > 1, ∀ n ≥ n0, c ^ n < (n - 1)! :=
+  let ⟨n0, h⟩ := (eventually_pow_lt_factorial_sub c 1).exists_forall_of_atTop
+  ⟨max n0 2, by omega, fun n hn ↦ h n (by omega)⟩
+
+@[deprecated eventually_mul_pow_lt_factorial_sub (since := "2024-09-25")]
+theorem exists_mul_pow_lt_factorial (a : ℕ) (c : ℕ) : ∃ n0, ∀ n ≥ n0, a * c ^ n < (n - 1)! :=
+  (eventually_mul_pow_lt_factorial_sub a c 1).exists_forall_of_atTop
+
+end Nat

Mathlib/Order/Filter/AtTopBot/Floor.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2022 Yuyang Zhao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yuyang Zhao
+-/
+import Mathlib.Algebra.Order.Floor
+import Mathlib.Order.Filter.AtTopBot
+
+/-!
+# `a * c ^ n < (n - d)!` holds true for sufficiently large `n`.
+-/
+
+open Filter
+open scoped Nat
+
+variable {K : Type*} [LinearOrderedRing K] [FloorSemiring K]
+
+theorem FloorSemiring.eventually_mul_pow_lt_factorial_sub (a c : K) (d : ℕ) :
+    ∀ᶠ n in atTop, a * c ^ n < (n - d)! := by
+  filter_upwards [Nat.eventually_mul_pow_lt_factorial_sub ⌈|a|⌉₊ ⌈|c|⌉₊ d] with n h
+  calc a * c ^ n
+    _ ≤ |a * c ^ n| := le_abs_self _
+    _ ≤ ⌈|a|⌉₊ * (⌈|c|⌉₊ : K) ^ n := ?_
+    _ = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) := ?_
+    _ < (n - d)! := Nat.cast_lt.mpr h
+  · rw [abs_mul, abs_pow]
+    gcongr <;> try first | positivity | apply Nat.le_ceil
+  · simp_rw [Nat.cast_mul, Nat.cast_pow]

Mathlib/Topology/Algebra/Order/Floor.lean

@@ -3,9 +3,8 @@ Copyright (c) 2020 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import Mathlib.Algebra.Order.Floor
+import Mathlib.Order.Filter.AtTopBot.Floor
 import Mathlib.Topology.Algebra.Order.Group
-import Mathlib.Topology.Order.Basic
 
 /-!
 # Topological facts about `Int.floor`, `Int.ceil` and `Int.fract`
@@ -27,8 +26,36 @@ This file proves statements about limits and continuity of functions involving `
 
 open Filter Function Int Set Topology
 
+namespace FloorSemiring
+
+open scoped Nat
+
+variable {K : Type*} [LinearOrderedField K] [FloorSemiring K] [TopologicalSpace K] [OrderTopology K]
+
+theorem tendsto_mul_pow_div_factorial_sub_atTop (a c : K) (d : ℕ) :
+    Tendsto (fun n ↦ a * c ^ n / (n - d)!) atTop (𝓝 0) := by
+  rw [tendsto_order]
+  constructor
+  all_goals
+    intro ε hε
+    filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n h
+    rw [mul_right_comm, ← div_eq_mul_inv] at h
+  · rw [div_lt_iff_of_neg hε] at h
+    rwa [lt_div_iff₀' (Nat.cast_pos.mpr (Nat.factorial_pos _))]
+  · rw [div_lt_iff₀ hε] at h
+    rwa [div_lt_iff₀' (Nat.cast_pos.mpr (Nat.factorial_pos _))]
+
+theorem tendsto_pow_div_factorial_atTop (c : K) :
+    Tendsto (fun n ↦ c ^ n / n !) atTop (𝓝 0) := by
+  convert tendsto_mul_pow_div_factorial_sub_atTop 1 c 0
+  rw [one_mul]
+
+end FloorSemiring
+
 variable {α β γ : Type*} [LinearOrderedRing α] [FloorRing α]
 
+-- TODO: move to `Mathlib.Order.Filter.AtTopBot.Floor`
+
 theorem tendsto_floor_atTop : Tendsto (floor : α → ℤ) atTop atTop :=
   floor_mono.tendsto_atTop_atTop fun b =>
     ⟨(b + 1 : ℤ), by rw [floor_intCast]; exact (lt_add_one _).le⟩