Analysis I, Section 9.4: Continuous functions

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, using the Mathlib notions

namespace Chapter9

Definition 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

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

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

Example 9.4.2 -

declaration uses 'sorry'example (c x₀:ℝ) : ContinuousWithinAt (fun x ↦ c) .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) .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! 🐙

Example 9.4.3 -

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

Example 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! 🐙

Example 9.4.5 -

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

Example 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 (.Ici 0) 0 := by⊢ ContinuousWithinAt f_9_4_6 (Set.Ici 0) 0 sorryAll goals completed! 🐙

Proposition 9.4.7 / Exercise 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.atTop.Tendsto a (nhds x₀) → Filter.atTop.Tendsto (fun n ↦ f (a n)) (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! 🐙

Remark 9.4.8 -

theorem _root_.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.atTop.Tendsto a (nhds x₀)):
  Filter.atTop.Tendsto (fun n ↦ f (a n)) (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:?_mvar.4281 := List.TFAE.out (ContinuousWithinAt.tfae _fvar.4270 _fvar.4271 _fvar.4273) 0 1 ?_mvar.4326 ?_mvar.4327⊢ Filter.Tendsto (fun n => f (a n)) Filter.atTop (nhds (f x₀))
  grindAll 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 [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₀; convert hf.add (AdherentPt.of_mem h) 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 [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₀; convert hf.sub (AdherentPt.of_mem h) 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 [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₀; convert hf.max (AdherentPt.of_mem h) 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 [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₀; convert hf.min (AdherentPt.of_mem h) 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 [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₀; convert hf.mul (AdherentPt.of_mem h) 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 [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₀; convert hf.div (AdherentPt.of_mem h) hM hg using 1All goals completed! 🐙

Proposition 9.4.10 / Exercise 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! 🐙

Proposition 9.4.11 / Exercise 9.4.4

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

Proposition 9.4.12

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

Proposition 9.4.13 / Exercise 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! 🐙

Example 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! 🐙

Exercise 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! 🐙

Exercise 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! 🐙