Documentation

Analysis.Section_6_7

Аналіз I, Розділ 6.7: Піднесення до дійсного степеня, частина II #

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

Оскільки дійсні числа з Розділу 5 застаріли на користь дійсних чисел із Mathlib, а операція піднесення до степеня в Mathlib визначена без попереднього введення раціональних степенів, ми приймемо дещо незручну компромісну позицію: спочатку використовуватимемо операцію піднесення з Mathlib (та її API), коли показник є раціональним, а цим скористаємось для визначення піднесення до дійсного степеня, і в епілозі до цього розділу ми покажемо, що це збігається з операцією Mathlib.

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

Лема 6.7.1 (Неперервність піднесення до степеня)

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 α : ℝ) :
ℝ

Визначення 6.7.2 (Піднесення до дійсного показника)

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

    Твердження 6.7.3(a) / Вправа 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

    Твердження 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)

    Твердження 6.7.3(b) / Вправа 6.7.1

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

    Твердження 6.7.3(c) / Вправа 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

    Твердження 6.7.3(d) / Вправа 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

    Твердження 6.7.3(e) / Вправа 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

    Твердження 6.7.3(e) / Вправа 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

    Твердження 6.7.3(f) / Вправа 6.7.1