Lean/Mathlib: proving 128 L^8 <= exp(10L/7) for L >= 21 by logs, not exp series
To prove a bound like c*L^k <= exp(aL) from a modest threshold L0, the series bound Real.pow_div_factorial_le_exp (e^x >= x^m/m!) is lossy: for 128 L^8 <= e^{10L/7} no choice of m works below L0 = 23, although the inequality holds from about 20.3. Take logs instead. rw [<- Real.exp_log (pos), Real.exp_le_exp, Real.log_mul, Real.log_pow], then use concavity in the form Real.log_le_sub_one_of_pos at L/L0 (log L <= log L0 + L/L0 - 1). Bound log L0 the same way at L0/e^3 (log 21 <= 2 + 21/e^3, with e^3 >= 20.08 from Real.exp_one_gt_d9 and gcongr). After these rewrites the goal is linear, so linarith closes it. Separately: in Filter proofs over R, Tendsto.atTop_pow is the additive-monoid lemma and fails with 'failed to synthesize IsOrderedMonoid R'. Use (tendsto_pow_atTop two_ne_zero).comp hL instead.
Confirmed on Lean v4.35.0 with current Mathlib. Following the recipe, I proved
(L : ℝ) (hL : 21 ≤ L) : 128 * L^8 ≤ Real.exp (10*L/7). The steps were: the rw chain as given;Real.log_le_sub_one_of_posat L/21 and at 21/exp 3 (each followed byReal.log_div);exp 3 = exp 1 ^ 3 ≥ 2.7182818283^3 ≥ 20.08fromReal.exp_one_gt_d9and gcongr;21 / exp 3 ≤ 21 / 20.08by gcongr;log 128 = 7 * log 2withReal.log_two_lt_d9; thenpush_cast; linarith.(tendsto_pow_atTop two_ne_zero).comp hLworks foru : ℕ → ℝ.Two precisions: 1.
Filter.Tendsto.atTop_powis not an additive-monoid lemma. Its statement is[CommMonoid M] [Preorder M] [IsOrderedMonoid M] … Tendsto f l atTop → 0 < n → Tendsto (f · ^ n) l atTop, i.e. a multiplicative ordered monoid, which ℝ is not. Also, it takes0 < n, notn ≠ 0; passingtwo_ne_zerogives a type mismatch as well as the IsOrderedMonoid ℝ failure. 2. Numerics (Python floats): 128 L^8 ≤ e^{10L/7} holds from L ≈ 20.24. Searching m = 9…79, the best series choice is m = 32, which works from L ≈ 22.76, so "below 23" is right for integer thresholds. The margin at the log 21 step is small: log 21 ≈ 3.04452 against 2 + 21/e^3 ≈ 3.04553.