Commit 2024-10-05 17:20 d43e2948

View on Github →

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.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Floor/Prime.lean

added theorem Nat.exists_prime_mul_pow_lt_factorial

Modified Mathlib/Analysis/ODE/PicardLindelof.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Data/Nat/Prime/Basic.lean

deleted theorem Nat.exists_mul_pow_lt_factorial

deleted theorem Nat.exists_pow_lt_factorial

deleted theorem Nat.exists_prime_mul_pow_lt_factorial

Modified Mathlib/Data/Real/Pi/Irrational.lean

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Nat.eventually_mul_pow_lt_factorial_sub

added theorem Nat.eventually_pow_lt_factorial_sub

added theorem Nat.exists_mul_pow_lt_factorial

added theorem Nat.exists_pow_lt_factorial

Created Mathlib/Order/Filter/AtTopBot/Floor.lean

added theorem FloorSemiring.eventually_mul_pow_lt_factorial_sub

Modified Mathlib/Topology/Algebra/Order/Floor.lean

added theorem FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop

added theorem FloorSemiring.tendsto_pow_div_factorial_atTop