Аналіз I, Глава 9.4

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:

Continuity of functions

namespace Chapter9

Визначення 9.4.1. Here we use the Mathlib definition of continuity. The hypothesis unknown identifier 'x'sorry ∈ sorry : Propx ∈ unknown identifier 'X'X is not needed!

theorem ContinuousWithinAt.iff (X:Set ℝ) (f: ℝ → ℝ)  (x₀:ℝ) :
  ContinuousWithinAt f X x₀ ↔ Convergesto X f (f x₀) x₀ := byX:Set ℝf:ℝ → ℝx₀:ℝ⊢ ContinuousWithinAt f X x₀ ↔ Convergesto X f (f x₀) x₀
  rw [ContinuousWithinAt.eq_1, Convergesto.iff, nhdsWithin.eq_1]All goals completed! 🐙

ContinuousOn.eq_1.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y)
  (s : Set X) : ContinuousOn f s = ∀ x ∈ s, ContinuousWithinAt f s x#check ContinuousOn.eq_1

ContinuousOn.eq_1.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y)
  (s : Set X) : ContinuousOn f s = ∀ x ∈ s, ContinuousWithinAt f s x

continuous_iff_continuousOn_univ.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β]
  {f : α → β} : Continuous f ↔ ContinuousOn f Set.univ#check continuous_iff_continuousOn_univ

continuous_iff_continuousOn_univ.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β]
  {f : α → β} : Continuous f ↔ ContinuousOn f Set.univ

continuousWithinAt_univ.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β)
  (x : α) : ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x#check continuousWithinAt_univ

continuousWithinAt_univ.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β)
  (x : α) : ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x

Приклад 9.4.2 -

declaration uses 'sorry'example (c x₀:ℝ) : ContinuousWithinAt (fun x ↦ c) Set.univ x₀ := byc:ℝx₀:ℝ⊢ ContinuousWithinAt (fun x => c) Set.univ x₀ sorryAll goals completed! 🐙

declaration uses 'sorry'example (c x₀:ℝ) : ContinuousAt (fun x ↦ c) x₀ := byc:ℝx₀:ℝ⊢ ContinuousAt (fun x => c) x₀ sorryAll goals completed! 🐙

declaration uses 'sorry'example (c:ℝ) : ContinuousOn (fun x:ℝ ↦ c) Set.univ := byc:ℝ⊢ ContinuousOn (fun x => c) Set.univ sorryAll goals completed! 🐙

declaration uses 'sorry'example (c:ℝ) : Continuous (fun x:ℝ ↦ c) := byc:ℝ⊢ Continuous fun x => c sorryAll goals completed! 🐙

Приклад 9.4.3 -

declaration uses 'sorry'example : Continuous (fun x:ℝ ↦ x) := by⊢ Continuous fun x => x sorryAll goals completed! 🐙

Приклад 9.4.4 -

declaration uses 'sorry'example {x₀:ℝ} (h: x₀ ≠ 0) : ContinuousAt Real.sign x₀ := byx₀:ℝh:x₀ ≠ 0⊢ ContinuousAt Real.sign x₀ sorryAll goals completed! 🐙

declaration uses 'sorry'example  :¬ ContinuousAt Real.sign 0 := by⊢ ¬ContinuousAt Real.sign 0 sorryAll goals completed! 🐙

Приклад 9.4.5 -

declaration uses 'sorry'example (x₀:ℝ) : ¬ ContinuousAt f_9_3_21 x₀ := byx₀:ℝ⊢ ¬ContinuousAt f_9_3_21 x₀ sorryAll goals completed! 🐙

Приклад 9.4.6 -

noncomputable abbrev f_9_4_6 (x:ℝ) : ℝ := if x ≥ 0 then 1 else 0

declaration uses 'sorry'example {x₀:ℝ} (h: x₀ ≠ 0) : ContinuousAt f_9_4_6 x₀ := byx₀:ℝh:x₀ ≠ 0⊢ ContinuousAt f_9_4_6 x₀ sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ ContinuousAt f_9_4_6 0 := by⊢ ¬ContinuousAt f_9_4_6 0 sorryAll goals completed! 🐙

declaration uses 'sorry'example : ContinuousWithinAt f_9_4_6 (Set.Ici 0) 0 := by⊢ ContinuousWithinAt f_9_4_6 (Set.Ici 0) 0 sorryAll goals completed! 🐙

Твердження 9.4.7 / Вправа 9.4.1. It is possible that the hypothesis unknown identifier 'x₀'sorry ∈ sorry : Propx₀ ∈ unknown identifier 'X'X is unnecessary.

theorem declaration uses 'sorry'ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) :
  [
    ContinuousWithinAt f X x₀,
    ∀ a:ℕ → ℝ, (∀ n, a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦  f (a n)) Filter.atTop (nhds (f x₀)),
    ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x-x₀| < δ → |f x - f x₀| < ε
  ].TFAE := byX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ X⊢ [ContinuousWithinAt f X x₀,
    ∀ (a : ℕ → ℝ),
      (∀ (n : ℕ), a n ∈ X) →
        Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (f x₀)),
    ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε].TFAE
  sorryAll goals completed! 🐙

Ремарка 9.4.8 -

theorem Filter.Tendsto.comp_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h : x₀ ∈ X)
  (h_cont: ContinuousWithinAt f X x₀) {a: ℕ → ℝ} (ha: ∀ n, a n ∈ X)
  (hconv: Filter.Tendsto a Filter.atTop (nhds x₀)):
  Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds (f x₀)) := byX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xh_cont:ContinuousWithinAt f X x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Xhconv:Filter.Tendsto a Filter.atTop (nhds x₀)⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (f x₀))
  have := (ContinuousWithinAt.tfae X f h).out 0 1X:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xh_cont:ContinuousWithinAt f X x₀a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Xhconv:Filter.Tendsto a Filter.atTop (nhds x₀)this:ContinuousWithinAt f X x₀ ↔
  ∀ (a : ℕ → ℝ),
    (∀ (n : ℕ), a n ∈ X) →
      Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (f x₀))⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (f x₀))
  rw [this] at h_contX:Set ℝf:ℝ → ℝx₀:ℝh:x₀ ∈ Xh_cont:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X) →
    Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (f x₀))a:ℕ → ℝha:∀ (n : ℕ), a n ∈ Xhconv:Filter.Tendsto a Filter.atTop (nhds x₀)this:ContinuousWithinAt f X x₀ ↔
  ∀ (a : ℕ → ℝ),
    (∀ (n : ℕ), a n ∈ X) →
      Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (f x₀))⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (f x₀))
  exact h_cont a ha hconvAll goals completed! 🐙

/- Proposition 9.4.9 -/
theorem ContinuousWithinAt.add {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
  (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
  ContinuousWithinAt (f + g) X x₀ := byX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:ContinuousWithinAt f X x₀hg:ContinuousWithinAt g X x₀⊢ ContinuousWithinAt (f + g) X x₀
  rw [ContinuousWithinAt.iff] at hf hg ⊢X:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀⊢ Convergesto X (f + g) ((f + g) x₀) x₀
  have had := AdherentPt.of_mem hX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀had:AdherentPt x₀ X⊢ Convergesto X (f + g) ((f + g) x₀) x₀
  convert Convergesto.add had hf hg using 1All goals completed! 🐙

theorem ContinuousWithinAt.sub {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
  (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
  ContinuousWithinAt (f - g) X x₀ := byX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:ContinuousWithinAt f X x₀hg:ContinuousWithinAt g X x₀⊢ ContinuousWithinAt (f - g) X x₀
  rw [ContinuousWithinAt.iff] at hf hg ⊢X:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀⊢ Convergesto X (f - g) ((f - g) x₀) x₀
  have had := AdherentPt.of_mem hX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀had:AdherentPt x₀ X⊢ Convergesto X (f - g) ((f - g) x₀) x₀
  convert Convergesto.sub had hf hg using 1All goals completed! 🐙

theorem ContinuousWithinAt.max {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
  (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
  ContinuousWithinAt (max f g) X x₀ := byX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:ContinuousWithinAt f X x₀hg:ContinuousWithinAt g X x₀⊢ ContinuousWithinAt (f ⊔ g) X x₀
  rw [ContinuousWithinAt.iff] at hf hg ⊢X:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀⊢ Convergesto X (f ⊔ g) (Max.max f g x₀) x₀
  have had := AdherentPt.of_mem hX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀had:AdherentPt x₀ X⊢ Convergesto X (f ⊔ g) (Max.max f g x₀) x₀
  convert Convergesto.max had hf hg using 1All goals completed! 🐙

theorem ContinuousWithinAt.min {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
  (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
  ContinuousWithinAt (min f g) X x₀ := byX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:ContinuousWithinAt f X x₀hg:ContinuousWithinAt g X x₀⊢ ContinuousWithinAt (f ⊓ g) X x₀
  rw [ContinuousWithinAt.iff] at hf hg ⊢X:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀⊢ Convergesto X (f ⊓ g) (Min.min f g x₀) x₀
  have had := AdherentPt.of_mem hX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀had:AdherentPt x₀ X⊢ Convergesto X (f ⊓ g) (Min.min f g x₀) x₀
  convert Convergesto.min had hf hg using 1All goals completed! 🐙

theorem ContinuousWithinAt.mul' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
  (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
  ContinuousWithinAt (f * g) X x₀ := byX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:ContinuousWithinAt f X x₀hg:ContinuousWithinAt g X x₀⊢ ContinuousWithinAt (f * g) X x₀
  rw [ContinuousWithinAt.iff] at hf hg ⊢X:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀⊢ Convergesto X (f * g) ((f * g) x₀) x₀
  have had := AdherentPt.of_mem hX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ Xhf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀had:AdherentPt x₀ X⊢ Convergesto X (f * g) ((f * g) x₀) x₀
  convert Convergesto.mul had hf hg using 1All goals completed! 🐙

theorem ContinuousWithinAt.div' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hM: g x₀ ≠ 0)
  (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
  ContinuousWithinAt (f / g) X x₀ := byX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ XhM:g x₀ ≠ 0hf:ContinuousWithinAt f X x₀hg:ContinuousWithinAt g X x₀⊢ ContinuousWithinAt (f / g) X x₀
  rw [ContinuousWithinAt.iff] at hf hg ⊢X:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ XhM:g x₀ ≠ 0hf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀⊢ Convergesto X (f / g) ((f / g) x₀) x₀
  have had := AdherentPt.of_mem hX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝh:x₀ ∈ XhM:g x₀ ≠ 0hf:Convergesto X f (f x₀) x₀hg:Convergesto X g (g x₀) x₀had:AdherentPt x₀ X⊢ Convergesto X (f / g) ((f / g) x₀) x₀
  convert Convergesto.div had hM hf hg using 1All goals completed! 🐙

Твердження 9.4.10 / Вправа 9.4.3

theorem declaration uses 'sorry'Continuous.exp {a:ℝ} (ha: a>0) : Continuous (fun x:ℝ ↦ a ^ x) := bya:ℝha:a > 0⊢ Continuous fun x => a ^ x
  sorryAll goals completed! 🐙

Твердження 9.4.11 / Вправа 9.4.4

theorem declaration uses 'sorry'Continuous.exp' (p:ℝ) : ContinuousOn (fun x:ℝ ↦ x ^ p) (Set.Ioi 0) := byp:ℝ⊢ ContinuousOn (fun x => x ^ p) (Set.Ioi 0)
  sorryAll goals completed! 🐙

Твердження 9.4.12

theorem declaration uses 'sorry'Continuous.abs : Continuous (fun x:ℝ ↦ |x|) := by⊢ Continuous fun x => |x|
  sorryAll goals completed! 🐙 -- TODO

Твердження 9.4.13 / Вправа 9.4.5

theorem declaration uses 'sorry'ContinuousWithinAt.comp {X Y: Set ℝ} {f g:ℝ → ℝ} (hf: ∀ x ∈ X, f x ∈ Y) {x₀:ℝ} (hx₀: x ∈ X) (hf_cont: ContinuousWithinAt f X x₀) (hg_cont: ContinuousWithinAt g Y (f x₀)): ContinuousWithinAt (g ∘ f) X x₀ := byx:ℝX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhf:∀ x ∈ X, f x ∈ Yx₀:ℝhx₀:x ∈ Xhf_cont:ContinuousWithinAt f X x₀hg_cont:ContinuousWithinAt g Y (f x₀)⊢ ContinuousWithinAt (g ∘ f) X x₀ sorryAll goals completed! 🐙

Приклад 9.4.14

declaration uses 'sorry'example : Continuous (fun x:ℝ ↦ 3*x + 1) := by⊢ Continuous fun x => 3 * x + 1
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Continuous (fun x:ℝ ↦ (5:ℝ)^x) := by⊢ Continuous fun x => 5 ^ x
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Continuous (fun x:ℝ ↦ (5:ℝ)^(3*x+1)) := by⊢ Continuous fun x => 5 ^ (3 * x + 1)
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Continuous (fun x:ℝ ↦ |x^2-8*x+8|^(Real.sqrt 2) / (x^2 + 1)) := by⊢ Continuous fun x => |x ^ 2 - 8 * x + 8| ^ √2 / (x ^ 2 + 1)
  sorryAll goals completed! 🐙

Вправа 9.4.6

theorem declaration uses 'sorry'ContinuousOn.restrict {X Y:Set ℝ} {f: ℝ → ℝ} (hY: Y ⊆ X) (hf: ContinuousOn f X) : ContinuousOn f Y := byX:Set ℝY:Set ℝf:ℝ → ℝhY:Y ⊆ Xhf:ContinuousOn f X⊢ ContinuousOn f Y
  sorryAll goals completed! 🐙

Вправа 9.4.7

theorem declaration uses 'sorry'Continuous.polynomial {n:ℕ} (c: Fin n → ℝ) : Continuous (fun x:ℝ ↦ ∑ i, c i * x ^ (i:ℕ)) := byn:ℕc:Fin n → ℝ⊢ Continuous fun x => ∑ i, c i * x ^ ↑i
  sorryAll goals completed! 🐙