noncomputable def realExpSeries (x : ℝ) : ℝ

Definition 4.5.1 (Exponential function): for every real number x, the exponential function is given by the power series exp(x) := ∑' n : ℕ, x^n / n!.

Equations

• realExpSeries x = ∑' (n : ℕ), x ^ n / ↑n.factorial

noncomputable def realEulerNumber : ℝ

Definition 4.5.2 (Euler's number): Euler's number e is the real number defined by e := exp(1), with series expansion e = ∑' n : ℕ, 1 / n!.

Equations

• realEulerNumber = Real.exp 1

noncomputable def naturalLog : ↑(Set.Ioi 0) → ℝ

Definition 4.5.3 (Natural logarithm): the natural logarithm is the function log : (0, ∞) → ℝ, also denoted ln, defined as the inverse of exp : ℝ → (0, ∞).

Equations

• naturalLog x = Real.log ↑x

theorem naturalLog_inverse_exp : (∀ (x : ↑(Set.Ioi 0)), Real.exp (naturalLog x) = ↑x) ∧ ∀ (y : ℝ), naturalLog ⟨Real.exp y, ⋯⟩ = y

The restricted natural logarithm and exponential satisfy exp (naturalLog x) = x for x > 0 and naturalLog (exp y) = y.

theorem summable_one_div_factorial : Summable fun (n : ℕ) => 1 / ↑n.factorial

The defining series ∑ n, 1 / n! for Euler's number is summable in ℝ.

theorem realEulerNumber_eq_tsum : realEulerNumber = ∑' (n : ℕ), 1 / ↑n.factorial

Series characterization of Euler's number via the exponential series at x = 1.

theorem helperForProposition_4_5_1_exp_eq_expOne_rpow (x : ℝ) : Real.exp x = Real.exp 1 ^ x

Helper for Proposition 4.5.1: rewrite Real.exp x as (Real.exp 1) ^ x.

theorem helperForProposition_4_5_1_realEulerNumber_rpow_rewrite (x : ℝ) : Real.exp 1 ^ x = realEulerNumber ^ x

Helper for Proposition 4.5.1: rewrite (Real.exp 1) ^ x using realEulerNumber.

theorem real_exp_eq_eulerNumber_rpow (x : ℝ) : Real.exp x = realEulerNumber ^ x

Proposition 4.5.1: for every real number x, the exponential function satisfies Real.exp x = realEulerNumber ^ x (that is, exp(x) = e^x).

theorem exp_basic_properties_part_a : (∀ (x : ℝ), Summable fun (n : ℕ) => |x ^ n / ↑n.factorial|) ∧ (∀ (x : ℝ), Real.exp x = ∑' (n : ℕ), x ^ n / ↑n.factorial) ∧ (NormedSpace.expSeries ℝ ℝ).radius = ⊤ ∧ AnalyticOn ℝ Real.exp Set.univ

Theorem 4.5.1 (Basic properties of exp, part (a)): for every real number x, the series ∑' n : ℕ, x^n / n! is absolutely convergent. In particular, Real.exp x = ∑' n : ℕ, x^n / n! for all x, the associated power series has infinite radius of convergence, and Real.exp is real analytic on ℝ.

theorem exp_basic_properties_part_b : Differentiable ℝ Real.exp ∧ ∀ (x : ℝ), deriv Real.exp x = Real.exp x

Theorem 4.5.2 (Basic properties of exp, part (b)): the function exp : ℝ → ℝ is differentiable on ℝ, and for every x : ℝ, we have exp'(x) = exp(x).

theorem exp_basic_properties_part_c : Continuous Real.exp ∧ ∀ (a b : ℝ), ∫ (x : ℝ) in a..b, Real.exp x = Real.exp b - Real.exp a

Theorem 4.5.3 (Basic properties of exp, part (c)): the function exp is continuous on ℝ. Moreover, for every a, b : ℝ, ∫ x in a..b, exp x = exp b - exp a.

theorem exp_basic_properties_part_d (x y : ℝ) : Real.exp (x + y) = Real.exp x * Real.exp y

Theorem 4.5.4 (Basic properties of exp, part (d)): for all x, y : ℝ, exp (x + y) = exp x * exp y.

theorem exp_basic_properties_part_e : Real.exp 0 = 1 ∧ ∀ (x : ℝ), Real.exp x > 0 ∧ Real.exp (-x) = 1 / Real.exp x

Theorem 4.5.5 (Basic properties of exp, part (e)): exp 0 = 1. Moreover, for every x : ℝ, we have exp x > 0 and exp (-x) = 1 / exp x.

theorem exp_basic_properties_part_f : StrictMono Real.exp ∧ ∀ (x y : ℝ), y > x ↔ Real.exp y > Real.exp x

Theorem 4.5.6 (Basic properties of exp, part (f)): the function exp is strictly increasing on ℝ. Equivalently, for all x, y : ℝ, y > x ↔ Real.exp y > Real.exp x.

theorem helperForTheorem_4_5_7_deriv_log_of_pos (x : ℝ) (_hx : 0 < x) : deriv Real.log x = 1 / x

Helper for Theorem 4.5.7: derivative of Real.log at positive inputs.

theorem helperForTheorem_4_5_7_rightEndpoint_pos (a b : ℝ) (ha : 0 < a) (hab : a < b) : 0 < b

Helper for Theorem 4.5.7: positivity of the right endpoint from 0 < a < b.

theorem helperForTheorem_4_5_7_integral_one_div_eq_log_div (a b : ℝ) (ha : 0 < a) (hab : a < b) : ∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)

Helper for Theorem 4.5.7: integral of 1 / x on a positive interval.

theorem helperForTheorem_4_5_7_log_div_eq_sub (a b : ℝ) (ha : 0 < a) (hab : a < b) : Real.log (b / a) = Real.log b - Real.log a

Helper for Theorem 4.5.7: convert log (b / a) into log b - log a.

theorem logarithm_properties_part_a : (∀ (x : ℝ), 0 < x → deriv Real.log x = 1 / x) ∧ ∀ (a b : ℝ), 0 < a → a < b → ∫ (x : ℝ) in a..b, 1 / x = Real.log b - Real.log a

Theorem 4.5.7 (Logarithm properties, part (a)): for every x > 0, the derivative of ln is ln'(x) = 1 / x. In particular, for any 0 < a < b, ∫ x in a..b, (1 / x) = ln(b) - ln(a).

theorem logarithm_properties_part_b (x y : ℝ) : 0 < x → 0 < y → Real.log (x * y) = Real.log x + Real.log y

Theorem 4.5.8 (Logarithm properties, part (b)): for all x, y > 0, ln (xy) = ln x + ln y.

theorem helperForTheorem_4_5_9_log_one : Real.log 1 = 0

Helper for Theorem 4.5.9: the logarithm of 1 is 0.

theorem helperForTheorem_4_5_9_log_one_div_eq_neg_log (x : ℝ) : Real.log (1 / x) = -Real.log x

Helper for Theorem 4.5.9: reciprocal inside log gives negation.

theorem helperForTheorem_4_5_9_log_one_div_eq_neg_log_of_pos (x : ℝ) (_hx : 0 < x) : Real.log (1 / x) = -Real.log x

Helper for Theorem 4.5.9: the reciprocal-log identity in the x > 0 form.

theorem logarithm_properties_part_c : Real.log 1 = 0 ∧ ∀ (x : ℝ), 0 < x → Real.log (1 / x) = -Real.log x

Theorem 4.5.9 (Logarithm properties, part (c)): ln(1) = 0. Moreover, for every x > 0, ln(1 / x) = -ln(x).

theorem helperForTheorem_4_5_10_rpow_def_of_pos {x y : ℝ} (hx : 0 < x) : x ^ y = Real.exp (y * Real.log x)

Helper for Theorem 4.5.10: rewrite x ^ y with the exp (y * log x) definition when x > 0.

theorem helperForTheorem_4_5_10_log_rpow_of_pos {x y : ℝ} (hx : 0 < x) : Real.log (x ^ y) = y * Real.log x

Helper for Theorem 4.5.10: the logarithm of a real power for positive base.

theorem logarithm_properties_part_d (x y : ℝ) : 0 < x → Real.log (x ^ y) = y * Real.log x

Theorem 4.5.10 (Logarithm properties, part (d)): for any x > 0 and y : ℝ, one has ln (x^y) = y ln x, where x^y is defined by x^y = exp (y ln x).

theorem helperForTheorem_4_5_11_log_one_sub_eq_neg_tsum_of_mem_Ioo_neg_one_one {x : ℝ} (hx : x ∈ Set.Ioo (-1) 1) : Real.log (1 - x) = -∑' (n : ℕ), x ^ (n + 1) / ↑(n + 1)

Helper for Theorem 4.5.11: the logarithm series identity on (-1, 1).

theorem helperForTheorem_4_5_11_term_rewrite_center_one (x : ℝ) (n : ℕ) : (-1) ^ n / ↑(n + 1) * (x - 1) ^ (n + 1) = -((1 - x) ^ (n + 1) / ↑(n + 1))

Helper for Theorem 4.5.11: rewrite the centered logarithm-series term.

theorem helperForTheorem_4_5_11_log_eq_and_summable_inside_radius {x : ℝ} (hx : x ∈ Set.Ioo 0 2) : Real.log x = ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) * (x - 1) ^ (n + 1) ∧ Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1) * (x - 1) ^ (n + 1)

Helper for Theorem 4.5.11: on (0, 2), log equals its centered power series at 1, and that series is summable.

theorem helperForTheorem_4_5_11_not_summable_outside_radius {x : ℝ} (hx : 1 < |x - 1|) : ¬Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1) * (x - 1) ^ (n + 1)

Helper for Theorem 4.5.11: outside radius 1 about 1, the centered logarithm series is not summable.

theorem logarithm_properties_part_e : (∀ x ∈ Set.Ioo (-1) 1, Real.log (1 - x) = -∑' (n : ℕ), x ^ (n + 1) / ↑(n + 1)) ∧ AnalyticAt ℝ Real.log 1 ∧ (∀ x ∈ Set.Ioo 0 2, Real.log x = ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) * (x - 1) ^ (n + 1)) ∧ (∀ (x : ℝ), |x - 1| < 1 → Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1) * (x - 1) ^ (n + 1)) ∧ ∀ (x : ℝ), 1 < |x - 1| → ¬Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1) * (x - 1) ^ (n + 1)

theorem helperForProposition_4_5_2_abs_alternating_harmonic_term (n : ℕ) : |(-1) ^ n / ↑(n + 1)| = 1 / ↑(n + 1)

Helper for Proposition 4.5.2: each alternating-harmonic term has absolute value 1 / (n + 1).

theorem helperForProposition_4_5_2_summable_alternating_implies_summable_harmonic : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) → Summable fun (n : ℕ) => 1 / ↑n

Helper for Proposition 4.5.2: unconditional summability of the alternating harmonic series implies summability of the harmonic series.

theorem helperForProposition_4_5_2_not_summable_unconditional_alternating_harmonic : ¬Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)

Helper for Proposition 4.5.2: under Lean's default (unconditional) Summable, the alternating harmonic series is not summable.

theorem helperForProposition_4_5_2_target_conjunction_implies_not_summable : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2 → ¬Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)

Helper for Proposition 4.5.2: any putative witness of the target conjunction would force a Summable claim that is already refuted under Lean's unconditional Summable semantics on ℕ.

theorem helperForProposition_4_5_2_log_two_ne_zero : Real.log 2 ≠ 0

Helper for Proposition 4.5.2: Real.log 2 is nonzero.

theorem helperForProposition_4_5_2_tsum_eq_zero_unconditional : ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = 0

Helper for Proposition 4.5.2: under Lean's default unconditional Summable semantics on ℕ, the alternating-harmonic tsum is forced to be 0.

theorem helperForProposition_4_5_2_not_tsum_eq_log_two_unconditional : ¬∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2

Helper for Proposition 4.5.2: under Lean's default unconditional Summable semantics on ℕ, the asserted tsum = log 2 identity cannot hold.

theorem helperForProposition_4_5_2_target_conjunction_implies_log_two_eq_zero : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2 → Real.log 2 = 0

Helper for Proposition 4.5.2: any proof of the target conjunction forces Real.log 2 = 0 under unconditional tsum semantics.

theorem helperForProposition_4_5_2_target_conjunction_implies_false_via_log_two : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2 → False

Helper for Proposition 4.5.2: any proof of the target conjunction directly contradicts Real.log 2 ≠ 0.

theorem helperForProposition_4_5_2_not_target_conjunction_unconditional : ¬((Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2)

Helper for Proposition 4.5.2: the target conjunction is inconsistent under Lean's default (unconditional) Summable on ℕ.

theorem helperForProposition_4_5_2_target_conjunction_implies_summable_harmonic : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2 → Summable fun (n : ℕ) => 1 / ↑n

Helper for Proposition 4.5.2: any proof of the target conjunction would force summability of the (unshifted) harmonic series.

theorem helperForProposition_4_5_2_target_conjunction_implies_false_via_harmonic : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2 → False

Helper for Proposition 4.5.2: the target conjunction yields a contradiction with Real.not_summable_one_div_natCast.

theorem helperForProposition_4_5_2_not_target_conjunction_via_harmonic_divergence : ¬((Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2)

Helper for Proposition 4.5.2: contradiction with harmonic divergence yields direct negation of the target conjunction.

theorem helperForProposition_4_5_2_target_conjunction_iff_false : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2 ↔ False

Helper for Proposition 4.5.2: under Lean's default unconditional Summable semantics on ℕ, the target conjunction is equivalent to False.

theorem helperForProposition_4_5_2_unconditional_obstructions : (¬Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ¬∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2

Helper for Proposition 4.5.2: under Lean's default unconditional Summable semantics on ℕ, both asserted claims in the target conjunction are blocked.

theorem helperForProposition_4_5_2_partial_sums_tendsto_some_limit : ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i / ↑(i + 1)) Filter.atTop (nhds l)

Helper for Proposition 4.5.2: the alternating harmonic partial sums converge conditionally (as a limit of finite sums), even though unconditional Summable on ℕ fails for this series in Lean.

theorem helperForProposition_4_5_2_target_conjunction_implies_partial_sums_tendsto_log_two : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2 → Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i / ↑(i + 1)) Filter.atTop (nhds (Real.log 2))

Helper for Proposition 4.5.2: if the target conjunction held, then the ordered partial sums would converge to Real.log 2.

theorem helperForProposition_4_5_2_partial_sums_limit_unique {l₁ l₂ : ℝ} (h₁ : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i / ↑(i + 1)) Filter.atTop (nhds l₁)) (h₂ : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i / ↑(i + 1)) Filter.atTop (nhds l₂)) : l₁ = l₂

Helper for Proposition 4.5.2: the limit of alternating-harmonic partial sums, when it exists, is unique.

theorem helperForProposition_4_5_2_target_conjunction_forces_unique_limit_log_two (h : (Summable fun (n : ℕ) => (-1) ^ n / ↑(n + 1)) ∧ ∑' (n : ℕ), (-1) ^ n / ↑(n + 1) = Real.log 2) {l : ℝ} (hl : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i / ↑(i + 1)) Filter.atTop (nhds l)) : l = Real.log 2

Helper for Proposition 4.5.2: under the target conjunction, any candidate limit of alternating-harmonic partial sums must equal Real.log 2.

theorem alternating_harmonic_summable_and_tsum_eq_log_two : Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.range N, (-1) ^ n / ↑(n + 1)) Filter.atTop (nhds (Real.log 2))

Proposition 4.5.2: the alternating harmonic series converges to ln(2), encoded in Lean as convergence of ordered partial sums: ∑_{n=1}^∞ (-1)^{n+1}/n = ln(2) becomes Tendsto (fun N => ∑ n < N, (-1)^n/(n+1)) atTop (𝓝 (log 2)).