Documentation

Analysis.Section_6_7

Analysis I, Section 6.7: Real exponentiation, part II #

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Because the Chapter 5 reals have been deprecated in favor of the Mathlib reals, and Mathlib real exponentiation is defined without first going through rational exponentiation, we will adopt a somewhat awkward compromise, in that we will initially accept the Mathlib exponentiation operation (with all its API) when the exponent is a rational, and use this to define a notion of real exponentiation which in the epilogue to this chapter we will show is identical to the Mathlib operation.

source
theorem Chapter6.ratPow_continuous {x α : ℝ} (hx : x > 0) {q : ℕ → ℚ} (hq : (↑fun (n : ℕ) => ↑(q n)).TendsTo α) :
(↑fun (n : ℕ) => x ^ ↑(q n)).Convergent

Lemma 6.7.1 (Continuity of exponentiation)

source
theorem Chapter6.ratPow_lim_uniq {x α : ℝ} (hx : x > 0) {q q' : ℕ → ℚ} (hq : (↑fun (n : ℕ) => ↑(q n)).TendsTo α) (hq' : (↑fun (n : ℕ) => ↑(q' n)).TendsTo α) :
(lim ↑fun (n : ℕ) => x ^ ↑(q n)) = lim ↑fun (n : ℕ) => x ^ ↑(q' n)
source
theorem Chapter6.Real.eq_lim_of_rat (α : ℝ) :
∃ (q : ℕ → ℚ), (↑fun (n : ℕ) => ↑(q n)).TendsTo α
source
@[reducible, inline]
noncomputable abbrev Chapter6.Real.rpow (x α : ℝ) :
ℝ

Definition 6.7.2 (Exponentiation to a real exponent)

Equations
Instances For
    source
    theorem Chapter6.Real.rpow_eq_lim_ratPow {x α : ℝ} (hx : x > 0) {q : ℕ → ℚ} (hq : (↑fun (n : ℕ) => ↑(q n)).TendsTo α) :
    rpow x α = lim ↑fun (n : ℕ) => x ^ ↑(q n)
    source
    theorem Chapter6.Real.ratPow_tendsto_rpow {x α : ℝ} (hx : x > 0) {q : ℕ → ℚ} (hq : (↑fun (n : ℕ) => ↑(q n)).TendsTo α) :
    (↑fun (n : ℕ) => x ^ ↑(q n)).TendsTo (rpow x α)
    source
    theorem Chapter6.Real.rpow_of_rat_eq_ratPow {x : ℝ} (hx : x > 0) {q : ℚ} :
    rpow x ↑q = x ^ ↑q
    source
    theorem Chapter6.Real.ratPow_nonneg {x : ℝ} (hx : x > 0) (q : ℝ) :
    rpow x q ≥ 0

    Proposition 6.7.3(a) / Exercise 6.7.1

    source
    theorem Chapter6.Real.ratPow_add {x : ℝ} (hx : x > 0) (q r : ℝ) :
    rpow x (q + r) = rpow x q * rpow x r

    Proposition 6.7.3(b)

    source
    theorem Chapter6.Real.ratPow_ratPow {x : ℝ} (hx : x > 0) (q r : ℝ) :
    rpow (rpow x q) r = rpow x (q * r)

    Proposition 6.7.3(b) / Exercise 6.7.1

    source
    theorem Chapter6.Real.ratPow_neg {x : ℝ} (hx : x > 0) (q : ℝ) :
    rpow x (-q) = 1 / rpow x q

    Proposition 6.7.3(c) / Exercise 6.7.1

    source
    theorem Chapter6.Real.ratPow_mono {x y : ℝ} (hx : x > 0) (hy : y > 0) {q : ℝ} (h : q > 0) :
    x > y ↔ rpow x q > rpow y q

    Proposition 6.7.3(d) / Exercise 6.7.1

    source
    theorem Chapter6.Real.ratPow_mono_of_gt_one {x : ℝ} (hx : x > 1) {q r : ℝ} :
    rpow x q > rpow x r ↔ q > r

    Proposition 6.7.3(e) / Exercise 6.7.1

    source
    theorem Chapter6.Real.ratPow_mono_of_lt_one {x : ℝ} (hx0 : 0 < x) (hx : x < 1) {q r : ℝ} :
    rpow x q < rpow x r ↔ q < r

    Proposition 6.7.3(e) / Exercise 6.7.1

    source
    theorem Chapter6.Real.ratPow_mul {x y : ℝ} (hx : x > 0) (hy : y > 0) (q : ℝ) :
    rpow (x * y) q = rpow x q * rpow y q

    Proposition 6.7.3(f) / Exercise 6.7.1