Аналіз I, Розділ 9.5: Ліві та праві границі

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

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

• Ліві та праві односторонні границі.

namespace Chapter9 open Classical in noncomputable abbrev right_limit (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : ℝ := if h : RightLimitExists X f x₀ then h.choose else 0abbrev LeftLimitExists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, (nhdsWithin x₀ (X ∩ .Iio x₀)).Tendsto f (nhds L)open Classical in noncomputable abbrev left_limit (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : ℝ := if h: LeftLimitExists X f x₀ then h.choose else 0theorem right_limit.eq {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {L:ℝ} (had: AdherentPt x₀ (X ∩ .Ioi x₀)) (h: (nhdsWithin x₀ (X ∩ .Ioi x₀)).Tendsto f (nhds L)) : RightLimitExists X f x₀ ∧ right_limit X f x₀ = L := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ RightLimitExists X f x₀ ∧ right_limit X f x₀ = L have h' : RightLimitExists X f x₀ := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ RightLimitExists X f x₀ ∧ right_limit X f x₀ = L use LAll goals completed! 🐙 simp [right_limit, h']X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)h':Chapter9.RightLimitExists _fvar.1432 _fvar.1433 _fvar.1434 := ?_mvar.1444⊢ Exists.choose ⋯ = L have hne : (nhdsWithin x₀ (X ∩ .Ioi x₀)).NeBot := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ RightLimitExists X f x₀ ∧ right_limit X f x₀ = L rwa [←mem_closure_iff_nhdsWithin_neBot, closure_def']X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)h':Chapter9.RightLimitExists _fvar.1432 _fvar.1433 _fvar.1434 := ?_mvar.1444⊢ AdherentPt x₀ (X ∩ Set.Ioi x₀) exact tendsto_nhds_unique h'.choose_spec hAll goals completed! 🐙theorem left_limit.eq {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {L:ℝ} (had: AdherentPt x₀ (X ∩ .Iio x₀)) (h: (nhdsWithin x₀ (X ∩ .Iio x₀)).Tendsto f (nhds L)) : LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L have h' : LeftLimitExists X f x₀ := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L use LAll goals completed! 🐙 simp [left_limit, h']X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)h':Chapter9.LeftLimitExists _fvar.3517 _fvar.3518 _fvar.3519 := ?_mvar.3529⊢ Exists.choose ⋯ = L have hne : (nhdsWithin x₀ (X ∩ .Iio x₀)).NeBot := byX:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L rwa [←mem_closure_iff_nhdsWithin_neBot, closure_def']X:Set ℝf:ℝ → ℝx₀:ℝL:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)h':Chapter9.LeftLimitExists _fvar.3517 _fvar.3518 _fvar.3519 := ?_mvar.3529⊢ AdherentPt x₀ (X ∩ Set.Iio x₀) exact tendsto_nhds_unique h'.choose_spec hAll goals completed! 🐙theorem right_limit.eq' {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: RightLimitExists X f x₀) : (nhdsWithin x₀ (X ∩ .Ioi x₀)).Tendsto f (nhds (right_limit X f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝh:RightLimitExists X f x₀⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀)) simp [right_limit, h]X:Set ℝf:ℝ → ℝx₀:ℝh:RightLimitExists X f x₀⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds (Exists.choose ⋯)); exact h.choose_specAll goals completed! 🐙theorem left_limit.eq' {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: LeftLimitExists X f x₀) : (nhdsWithin x₀ (X ∩ .Iio x₀)).Tendsto f (nhds (left_limit X f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝh:LeftLimitExists X f x₀⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀)) simp [left_limit, h]X:Set ℝf:ℝ → ℝx₀:ℝh:LeftLimitExists X f x₀⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds (Exists.choose ⋯)); exact h.choose_specAll goals completed! 🐙 declaration uses 'sorry'example : left_limit .univ Real.sign 0 = -1 := by⊢ left_limit Set.univ Real.sign 0 = -1 sorryAll goals completed! 🐙theorem right_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ .Ioi x₀)) (h: RightLimitExists X f x₀) (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ .Ioi x₀) (hconv: Filter.atTop.Tendsto a (nhds x₀)) : Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (right_limit X f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)h:RightLimitExists X f x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (right_limit X f x₀)) choose L hL using hX:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (right_limit X f x₀)) apply Convergesto.comp had _ ha hconvX:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ Convergesto (X ∩ Set.Ioi x₀) f (right_limit X f x₀) x₀ rwa [Convergesto.iff, (eq had hL).2]X:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Ioi x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ .Iio x₀)) (h: LeftLimitExists X f x₀) (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ .Iio x₀) (hconv: Filter.atTop.Tendsto a (nhds x₀)) : Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (left_limit X f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)h:LeftLimitExists X f x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (left_limit X f x₀)) choose L hL using hX:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (left_limit X f x₀)) apply Convergesto.comp had _ ha hconvX:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ Convergesto (X ∩ Set.Iio x₀) f (left_limit X f x₀) x₀ rwa [Convergesto.iff, (eq had hL).2]X:Set ℝf:ℝ → ℝx₀:ℝhad:AdherentPt x₀ (X ∩ Set.Iio x₀)a:ℕ → ℝha:∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀hconv:Filter.Tendsto a Filter.atTop (nhds x₀)L:ℝhL:Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)⊢ Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L) abbrev HasJumpDiscontinuity (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := RightLimitExists X f x₀ ∧ LeftLimitExists X f x₀ ∧ right_limit X f x₀ ≠ left_limit X f x₀declaration uses 'sorry'example : HasJumpDiscontinuity .univ Real.sign 0 := by⊢ HasJumpDiscontinuity Set.univ Real.sign 0 sorryAll goals completed! 🐙abbrev HasRemovableDiscontinuity (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := RightLimitExists X f x₀ ∧ LeftLimitExists X f x₀ ∧ right_limit X f x₀ = left_limit X f x₀ ∧ right_limit X f x₀ ≠ f x₀declaration uses 'sorry'example : HasRemovableDiscontinuity .univ f_9_3_17 0 := by⊢ HasRemovableDiscontinuity Set.univ f_9_3_17 0 sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ HasRemovableDiscontinuity .univ (fun x ↦ 1/x) 0 := by⊢ ¬HasRemovableDiscontinuity Set.univ (fun x => 1 / x) 0 sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ HasJumpDiscontinuity .univ (fun x ↦ 1/x) 0 := by⊢ ¬HasJumpDiscontinuity Set.univ (fun x => 1 / x) 0 sorryAll goals completed! 🐙/- Вправа 9.5.1: Запишіть визначення того, що означає, коли границя функції дорівнює `+∞` або `-∞`; застосуйте до `fun x ↦ 1/x`; сформулюйте й доведіть варіант Твердження 9.3.9. -/ end Chapter9