theorem helperForProposition_4_5_3_factorial_lower_bound_nat (n k : ℕ) : (n + 1).factorial * 2 ^ k ≤ (n + (k + 1)).factorial

Helper for Proposition 4.5.3: factorial tail denominator dominates a geometric factor.

theorem helperForProposition_4_5_3_term_le_geometric (n k : ℕ) : 1 / ↑(n + (k + 1)).factorial ≤ 1 / ↑(n + 1).factorial * (1 / 2) ^ k

Helper for Proposition 4.5.3: each factorial-tail term is bounded by a geometric term.

theorem helperForProposition_4_5_3_summable_tail (n : ℕ) : Summable fun (k : ℕ) => 1 / ↑(n + (k + 1)).factorial

Helper for Proposition 4.5.3: the shifted factorial reciprocal tail is summable.

theorem helperForProposition_4_5_3_tsum_le_two_div_factorial_succ (n : ℕ) : ∑' (k : ℕ), 1 / ↑(n + (k + 1)).factorial ≤ 2 / ↑(n + 1).factorial

Helper for Proposition 4.5.3: the shifted factorial reciprocal tail is bounded by a geometric sum equal to 2 / (n+1)!.

theorem helperForProposition_4_5_3_two_div_factorial_succ_lt_inv_factorial (n : ℕ) (hn : 3 ≤ n) : 2 / ↑(n + 1).factorial < 1 / ↑n.factorial

Helper for Proposition 4.5.3: the geometric upper bound is strictly below 1 / n! when n ≥ 3.

theorem factorial_tail_sum_pos_and_lt_inv_factorial (n : ℕ) (hn : 3 ≤ n) : 0 < ∑' (k : ℕ), 1 / ↑(n + (k + 1)).factorial ∧ ∑' (k : ℕ), 1 / ↑(n + (k + 1)).factorial < 1 / ↑n.factorial

Proposition 4.5.3: for every integer n ≥ 3, the factorial tail sum satisfies 0 < ∑' k : ℕ, 1 / (n + (k + 1))! < 1 / n!.

theorem helperForProposition_4_5_4_tsum_split_at_factorial_index (n : ℕ) : ∑' (j : ℕ), 1 / ↑j.factorial = ∑ j ∈ Finset.range (n + 1), 1 / ↑j.factorial + ∑' (k : ℕ), 1 / ↑(n + (k + 1)).factorial

Helper for Proposition 4.5.4: split the reciprocal-factorial series at index n+1.

theorem helperForProposition_4_5_4_factorialScaledFinitePart_isNatCast (n : ℕ) : ∃ (A : ℕ), ↑n.factorial * ∑ i ∈ Finset.range (n + 1), 1 / ↑i.factorial = ↑A

Helper for Proposition 4.5.4: after scaling the finite prefix by n!, one gets a natural-number cast.

theorem helperForProposition_4_5_4_factorialScaledTail_between_zero_one (n : ℕ) (hn : 3 ≤ n) : 0 < ↑n.factorial * ∑' (k : ℕ), 1 / ↑(n + (k + 1)).factorial ∧ ↑n.factorial * ∑' (k : ℕ), 1 / ↑(n + (k + 1)).factorial < 1

Helper for Proposition 4.5.4: scaling the factorial tail by n! yields a remainder in (0,1).

theorem helperForProposition_4_5_4_noInt_between_consecutiveIntCasts (z m : ℤ) : ¬(↑z < ↑m ∧ ↑m < ↑(z + 1))

Helper for Proposition 4.5.4: no integer cast lies strictly between two consecutive integer casts.

theorem factorial_mul_e_not_integer (n : ℕ) (hn : 3 ≤ n) : ¬∃ (m : ℤ), ↑n.factorial * realEulerNumber = ↑m

Proposition 4.5.4: for every integer n ≥ 3, the real number n! * e is not an integer.

theorem helperForProposition_4_5_5_cutoff_eq_expNegInvGlue : (fun (x : ℝ) => if 0 < x then Real.exp (-1 / x) else 0) = expNegInvGlue

Helper for Proposition 4.5.5: the cutoff definition coincides with expNegInvGlue.

theorem helperForProposition_4_5_5_contDiffTop_implies_analyticAt_zero {f : ℝ → ℝ} (hcont : ContDiff ℝ ⊤ f) : AnalyticAt ℝ f 0

Helper for Proposition 4.5.5: ContDiff ℝ ⊤ implies analyticity at 0.

theorem helperForProposition_4_5_5_target_conjunction_inconsistent : ¬have f := fun (x : ℝ) => if 0 < x then Real.exp (-1 / x) else 0; ContDiff ℝ ⊤ f ∧ (∀ (k : ℕ), iteratedDeriv k f 0 = 0) ∧ ¬AnalyticAt ℝ f 0

Helper for Proposition 4.5.5: as currently encoded, the target conjunction is inconsistent.

theorem helperForProposition_4_5_5_iteratedDeriv_zero_on_Iio (k : ℕ) : Set.EqOn (iteratedDeriv k fun (x : ℝ) => if 0 < x then Real.exp (-1 / x) else 0) (fun (x : ℝ) => 0) (Set.Iio 0)

Helper for Proposition 4.5.5: all iterated derivatives of the cutoff vanish on the negative half-line.

theorem helperForProposition_4_5_5_iteratedDeriv_zero_at_zero (hcont : ContDiff ℝ ↑⊤ fun (x : ℝ) => if 0 < x then Real.exp (-1 / x) else 0) (k : ℕ) : iteratedDeriv k (fun (x : ℝ) => if 0 < x then Real.exp (-1 / x) else 0) 0 = 0

Helper for Proposition 4.5.5: smoothness forces every iterated derivative of the cutoff to vanish at 0.

theorem helperForProposition_4_5_5_not_analytic_at_zero : ¬AnalyticAt ℝ (fun (x : ℝ) => if 0 < x then Real.exp (-1 / x) else 0) 0

Helper for Proposition 4.5.5: the cutoff is not analytic at 0.

theorem flat_exp_cutoff_smooth_all_derivs_zero_not_analytic_at_zero : have f := fun (x : ℝ) => if 0 < x then Real.exp (-1 / x) else 0; ContDiff ℝ (↑⊤) f ∧ (∀ (k : ℕ), iteratedDeriv k f 0 = 0) ∧ ¬AnalyticAt ℝ f 0

Proposition 4.5.5: define f : ℝ → ℝ by f x = exp (-1 / x) for x > 0 and f x = 0 for x ≤ 0. Then f is smooth on ℝ, all derivatives vanish at 0 (equivalently, for every integer k ≥ 0, f^(k)(0) = 0), and f is not real analytic at 0.

theorem helperForProposition_4_5_6_differentiable_of_analyticOn_univ {f : ℝ → ℝ} (hf_analytic : AnalyticOn ℝ f Set.univ) : Differentiable ℝ f

Helper for Proposition 4.5.6: analyticity on all of ℝ implies global differentiability.

theorem helperForProposition_4_5_6_deriv_log_eq_one {f : ℝ → ℝ} (hf_pos : ∀ (x : ℝ), 0 < f x) (hf_diff : Differentiable ℝ f) (hf_deriv : ∀ (x : ℝ), deriv f x = f x) (x : ℝ) : deriv (fun (y : ℝ) => Real.log (f y)) x = 1

Helper for Proposition 4.5.6: the derivative of log ∘ f is constantly 1.

theorem helperForProposition_4_5_6_log_sub_id_constant {f : ℝ → ℝ} (hf_pos : ∀ (x : ℝ), 0 < f x) (hf_diff : Differentiable ℝ f) (hf_deriv : ∀ (x : ℝ), deriv f x = f x) (x : ℝ) : Real.log (f x) - x = Real.log (f 0)

Helper for Proposition 4.5.6: x ↦ log (f x) - x is constant on ℝ.

theorem helperForProposition_4_5_6_exp_form {f : ℝ → ℝ} (hf_pos : ∀ (x : ℝ), 0 < f x) (hlog_const : ∀ (x : ℝ), Real.log (f x) - x = Real.log (f 0)) (x : ℝ) : f x = f 0 * Real.exp x

Helper for Proposition 4.5.6: the solution has the form f x = f 0 * exp x.

theorem analytic_deriv_eq_self_exists_pos_const_mul_exp {f : ℝ → ℝ} (hf_pos : ∀ (x : ℝ), 0 < f x) (hf_analytic : AnalyticOn ℝ f Set.univ) (hf_deriv : ∀ (x : ℝ), deriv f x = f x) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), f x = C * Real.exp x

Proposition 4.5.6: if f : ℝ → (0, ∞) is real analytic and satisfies f'(x) = f(x) for all x ∈ ℝ, then there exists a constant C > 0 such that f(x) = C e^x for all x ∈ ℝ.

theorem exp_div_pow_tendsto_atTop (m : ℕ) (hm : 1 ≤ m) : Filter.Tendsto (fun (x : ℝ) => Real.exp x / x ^ m) Filter.atTop Filter.atTop

Proposition 4.5.7: for every natural number m ≥ 1, lim_{x→+∞} (exp x / x^m) = +∞.

theorem helperForProposition_4_5_8_scaledEval_rewrite (P : Polynomial ℝ) {c : ℝ} (hc : 0 < c) (x : ℝ) : have Q := P.comp (Polynomial.C (1 / c) * Polynomial.X); Polynomial.eval (c * x) Q = Polynomial.eval x P

Helper for Proposition 4.5.8: rewriting the composed polynomial at a scaled input.

theorem helperForProposition_4_5_8_tendsto_div_exp_mul_atTop (P : Polynomial ℝ) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (x : ℝ) => Polynomial.eval x P / Real.exp (c * x)) Filter.atTop (nhds 0)

Helper for Proposition 4.5.8: the ratio P(x) / exp(c x) tends to 0 at +∞.

theorem helperForProposition_4_5_8_eventually_abs_lt_exp_mul (P : Polynomial ℝ) {c : ℝ} (hc : 0 < c) : ∀ᶠ (x : ℝ) in Filter.atTop, |Polynomial.eval x P| < Real.exp (c * x)

Helper for Proposition 4.5.8: eventually, |P(x)| is strictly below exp(c x).

theorem helperForProposition_4_5_8_eventually_atTop_to_threshold {R : ℝ → Prop} (hR : ∀ᶠ (x : ℝ) in Filter.atTop, R x) : ∃ (N : ℝ), ∀ x > N, R x

Helper for Proposition 4.5.8: convert an eventual atTop property into a threshold statement.

theorem exp_mul_gt_abs_polynomial_eventually (P : Polynomial ℝ) {c : ℝ} (hc : 0 < c) : ∃ (N : ℝ), ∀ x > N, Real.exp (c * x) > |Polynomial.eval x P|

Proposition 4.5.8: if P is a real polynomial and c > 0, then there exists N : ℝ such that for all real x > N, one has exp (c x) > |P(x)|.

theorem helperForProposition_4_5_9_continuous_baseCoordinate : Continuous fun (p : ↑(Set.Ioi 0) × ℝ) => ↑p.1

Helper for Proposition 4.5.9: continuity of the positive-base coordinate map.

theorem helperForProposition_4_5_9_rpow_sideCondition (p : ↑(Set.Ioi 0) × ℝ) : ↑p.1 ≠ 0 ∨ 0 < p.2

Helper for Proposition 4.5.9: the base in (0,+∞) is always nonzero.

theorem positive_rpow_map_continuous_on_Ioi_prod : Continuous fun (p : ↑(Set.Ioi 0) × ℝ) => ↑p.1 ^ p.2

Proposition 4.5.9: define f : (0,+∞) × ℝ → ℝ by f(x,y) = x^y, where x^y = exp (y ln x) for x > 0 and y ∈ ℝ; then f is continuous on (0,+∞) × ℝ.

theorem helperForTheorem_4_5_12_factorialDenominator_dvd_factorialMax (q : ℚ) : q.den ∣ (max 3 q.den).factorial

Helper for Theorem 4.5.12: the denominator of a rational divides (max 3 q.den)!.

theorem helperForTheorem_4_5_12_factorialScaledRat_isIntCast (q : ℚ) : ∃ (m : ℤ), ↑(max 3 q.den).factorial * ↑q = ↑m

Helper for Theorem 4.5.12: multiplying a rational by a suitable factorial gives an integer cast in ℝ.

theorem helperForTheorem_4_5_12_exp_one_ne_ratCast (q : ℚ) : Real.exp 1 ≠ ↑q

Helper for Theorem 4.5.12: exp 1 is not equal to any rational cast.

theorem realEulerNumber_irrational : Irrational (Real.exp 1)

Theorem 4.5.12: The number e is irrational.

theorem logarithm_real_analytic_on_Ioi : AnalyticOn ℝ Real.log (Set.Ioi 0)

Theorem 4.5.13: The natural logarithm function ln : (0,+∞) → ℝ is real analytic on (0,+∞).