Analysis II (Tao, 2022) -- Chapter 02 -- Section 01

section Chap02section Section01

Definition 2.1 (Continuous functions): (i) For Unknown identifier `x0`sorry ∈ sorry : Propx0 ∈ Unknown identifier `X`X, Unknown identifier `f`f is continuous at Unknown identifier `x0`x0 if for every Unknown identifier `ε`sorry > 0 : Propε > 0 there exists Unknown identifier `δ`sorry > 0 : Propδ > 0 such that for all Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `X`X, Unknown identifier `d_X`sorry < sorry : Propd_X x x0 < Unknown identifier `δ`δ implies Unknown identifier `d_Y`sorry < sorry : Propd_Y (f x) (f x0) < Unknown identifier `ε`ε. (ii) Unknown identifier `f`f is continuous on Unknown identifier `X`X if it is continuous at every Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `X`X.

abbrev IsContinuousAt {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x0 : X) : Prop := ContinuousAt f x0

A function between metric spaces is continuous if it is continuous at every point.

abbrev IsContinuous {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) : Prop := ∀ x : X, IsContinuousAt f x

Proposition 2.1: Let Unknown identifier `X`X be a topological space and let be continuous. Define by . Then Unknown identifier `f`sorry ^ 2 : ?m.6f^2 is continuous.

theorem continuous_sq_of_continuous {X : Type*} [TopologicalSpace X] (f : X → ℝ) : Continuous f → Continuous (fun x => (f x) ^ 2) := by intro hf simpa [pow_two] using hf.mul hf

Helper for Theorem 2.1: open-set formulation of continuity at a point.

lemma helperForTheorem_2_1_openImage_iff_continuousAt {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x0 : X) : IsContinuousAt f x0 ↔ ∀ V : Set Y, IsOpen V → f x0 ∈ V → ∃ U : Set X, IsOpen U ∧ x0 ∈ U ∧ f '' U ⊆ V := by constructor · intro hcont V hVopen hx0V have hcont' : ContinuousAt f x0 := by simpa [IsContinuousAt] using hcont have hVnhds : V ∈ nhds (f x0) := IsOpen.mem_nhds hVopen hx0V have hpre : f ⁻¹' V ∈ nhds x0 := (continuousAt_def (f:=f) (x:=x0)).1 hcont' V hVnhds rcases (mem_nhds_iff).1 hpre with ⟨U, hUsub, hUopen, hx0U⟩ refine ⟨U, hUopen, hx0U, ?_⟩ exact (Set.image_subset_iff).2 hUsub · intro hopen have hcont : ContinuousAt f x0 := by refine (continuousAt_def (f:=f) (x:=x0)).2 ?_ intro A hA rcases (mem_nhds_iff).1 hA with ⟨V, hVsub, hVopen, hx0V⟩ rcases hopen V hVopen hx0V with ⟨U, hUopen, hx0U, himage⟩ have hUsubV : U ⊆ f ⁻¹' V := (Set.image_subset_iff).1 himage have hUsubA : U ⊆ f ⁻¹' A := by intro x hx exact hVsub (hUsubV hx) exact (mem_nhds_iff).2 ⟨U, hUsubA, hUopen, hx0U⟩ simpa [IsContinuousAt] using hcont

Theorem 2.1 (Continuity preserves convergence): Let (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `X`X,Unknown identifier `d_X`d_X) and (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `Y`Y,Unknown identifier `d_Y`d_Y) be metric spaces, , and Unknown identifier `x0`sorry ∈ sorry : Propx0 ∈ Unknown identifier `X`X. The following statements are equivalent: (a) Unknown identifier `f`f is continuous at Unknown identifier `x0`x0. (b) For every sequence with Unknown identifier `x`sorry → sorry : Sort (imax u_1 u_2)x → Unknown identifier `x0`x0, one has Unknown identifier `f`f ∘ Unknown identifier `x`x → f x0. (c) For every open set Unknown identifier `V`sorry ⊆ sorry : PropV ⊆ Unknown identifier `Y`Y with Unknown identifier `f`sorry ∈ sorry : Propf x0 ∈ Unknown identifier `V`V, there exists an open set Unknown identifier `U`sorry ⊆ sorry : PropU ⊆ Unknown identifier `X`X with Unknown identifier `x0`sorry ∈ sorry : Propx0 ∈ Unknown identifier `U`U such that Unknown identifier `f`sorry '' sorry ⊆ sorry : Propf '' Unknown identifier `U`U ⊆ Unknown identifier `V`V.

theorem continuity_preserves_convergence {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x0 : X) : (IsContinuousAt f x0 ↔ ∀ x : ℕ → X, Filter.Tendsto x Filter.atTop (nhds x0) → Filter.Tendsto (fun n => f (x n)) Filter.atTop (nhds (f x0))) ∧ (IsContinuousAt f x0 ↔ ∀ V : Set Y, IsOpen V → f x0 ∈ V → ∃ U : Set X, IsOpen U ∧ x0 ∈ U ∧ f '' U ⊆ V) := by refine And.intro ?_ ?_ · simpa [IsContinuousAt, ContinuousAt, Function.comp] using (tendsto_nhds_iff_seq_tendsto (f:=f) (a:=x0) (b:=f x0)) · simpa using helperForTheorem_2_1_openImage_iff_continuousAt f x0

Proposition 2.2: Let (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `X`X, Unknown identifier `d`d) be a metric space and let be a subspace of (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `X`X, Unknown identifier `d`d). The inclusion map , defined by , is continuous.

theorem isContinuous_inclusion_subtype {X : Type*} [MetricSpace X] (E : Set X) : IsContinuous (Subtype.val : E → X) := by intro x simpa [IsContinuousAt] using (continuousAt_subtype_val (x:=x))

Helper for Theorem 2.2: IsContinuous.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) : PropIsContinuous matches Continuous.{u, v} {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : PropContinuous for metric spaces.

lemma helperForTheorem_2_2_isContinuous_iff_continuous {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) : IsContinuous f ↔ Continuous f := by constructor · intro hcont refine (continuous_iff_continuousAt (f:=f)).2 ?_ intro x0 have hcontAt : IsContinuousAt f x0 := hcont x0 simpa [IsContinuousAt] using hcontAt · Try this: intro hcont x0intro hcont intro x0 have hcontAt : ContinuousAt f x0 := (continuous_iff_continuousAt (f:=f)).1 hcont x0 simpa [IsContinuousAt] using hcontAt

Theorem 2.2: Let (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `X`X, Unknown identifier `d_X`d_X) and (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `Y`Y, Unknown identifier `d_Y`d_Y) be metric spaces and . The following statements are equivalent: (a) Unknown identifier `f`f is continuous. (b) Whenever a sequence Unknown identifier `x`x in Unknown identifier `X`X converges to Unknown identifier `x0`x0, the sequence fun n => sorry : (n : ?m.1) → ?m.3 nfun n => Unknown identifier `f`f (x n) converges to Unknown identifier `f`f x0. (c) For every open set Unknown identifier `V`sorry ⊆ sorry : PropV ⊆ Unknown identifier `Y`Y, the preimage Unknown identifier `f`sorry ⁻¹' sorry : Set ?m.1f ⁻¹' Unknown identifier `V`V is open in Unknown identifier `X`X. (d) For every closed set Unknown identifier `F`sorry ⊆ sorry : PropF ⊆ Unknown identifier `Y`Y, the preimage Unknown identifier `f`sorry ⁻¹' sorry : Set ?m.1f ⁻¹' Unknown identifier `F`F is closed in Unknown identifier `X`X.

theorem continuous_iff_sequential_iff_preimage_open_iff_preimage_closed {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) : (IsContinuous f ↔ ∀ x0 : X, ∀ x : ℕ → X, Filter.Tendsto x Filter.atTop (nhds x0) → Filter.Tendsto (fun n => f (x n)) Filter.atTop (nhds (f x0))) ∧ (IsContinuous f ↔ ∀ V : Set Y, IsOpen V → IsOpen (f ⁻¹' V)) ∧ (IsContinuous f ↔ ∀ F : Set Y, IsClosed F → IsClosed (f ⁻¹' F)) := by refine And.intro ?_ (And.intro ?_ ?_) · constructor · intro hcont x0 x hx have hcontAt : IsContinuousAt f x0 := hcont x0 have hseqEquiv := (continuity_preserves_convergence f x0).1 have hseq : ∀ x : ℕ → X, Filter.Tendsto x Filter.atTop (nhds x0) → Filter.Tendsto (fun n => f (x n)) Filter.atTop (nhds (f x0)) := hseqEquiv.mp hcontAt exact hseq x hx · intro hseq x0 have hseqAt : ∀ x : ℕ → X, Filter.Tendsto x Filter.atTop (nhds x0) → Filter.Tendsto (fun n => f (x n)) Filter.atTop (nhds (f x0)) := hseq x0 have hseqEquiv := (continuity_preserves_convergence f x0).1 exact hseqEquiv.mpr hseqAt · constructor · intro hcont V hV have hcont' : Continuous f := (helperForTheorem_2_2_isContinuous_iff_continuous f).1 hcont exact (continuous_def (f:=f)).1 hcont' V hV · intro hopen have hcont' : Continuous f := by refine (continuous_def (f:=f)).2 ?_ intro V hV exact hopen V hV exact (helperForTheorem_2_2_isContinuous_iff_continuous f).2 hcont' · constructor · intro hcont F hF have hcont' : Continuous f := (helperForTheorem_2_2_isContinuous_iff_continuous f).1 hcont exact (continuous_iff_isClosed (f:=f)).1 hcont' F hF · intro hclosed have hcont' : Continuous f := by refine (continuous_iff_isClosed (f:=f)).2 ?_ intro F hF exact hclosed F hF exact (helperForTheorem_2_2_isContinuous_iff_continuous f).2 hcont'

Helper for Proposition 2.3: continuity at a point is preserved under restriction to a subset.

lemma helperForProposition_2_3_restrict_isContinuousAt {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (E : Set X) (x0 : E) : IsContinuousAt f x0 → IsContinuousAt (fun x : E => f x) x0 := by intro hcont have hcont' : ContinuousAt f x0 := by simpa [IsContinuousAt] using hcont have hcomp : ContinuousAt (fun x : E => f x) x0 := hcont'.comp (continuousAt_subtype_val (x:=x0)) simpa [IsContinuousAt] using hcomp

Helper for Proposition 2.3: global continuity is preserved under restriction to a subset.

lemma helperForProposition_2_3_restrict_isContinuous {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (E : Set X) : IsContinuous f → IsContinuous (fun x : E => f x) := by intro hcont x0 have hcontAt : IsContinuousAt f x0 := hcont x0 exact helperForProposition_2_3_restrict_isContinuousAt f E x0 hcontAt

Proposition 2.3: If is continuous at Unknown identifier `x0`sorry ∈ sorry : Propx0 ∈ Unknown identifier `E`E, then the restriction is continuous at Unknown identifier `x0`x0; in particular, if Unknown identifier `f`f is continuous on Unknown identifier `X`X, then is continuous on Unknown identifier `E`E.

theorem continuous_restrict_of_continuous {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (E : Set X) : (∀ x0 : E, IsContinuousAt f x0 → IsContinuousAt (fun x : E => f x) x0) ∧ (IsContinuous f → IsContinuous (fun x : E => f x)) := by constructor · intro x0 hcont exact helperForProposition_2_3_restrict_isContinuousAt f E x0 hcont · intro hcont exact helperForProposition_2_3_restrict_isContinuous f E hcont

Theorem 2.3 (Continuity preserved by composition): Let (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `X`X,Unknown identifier `d_X`d_X), (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `Y`Y,Unknown identifier `d_Y`d_Y), and (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `Z`Z,Unknown identifier `d_Z`d_Z) be metric spaces. (a) If is continuous at Unknown identifier `x0`x0 and is continuous at Unknown identifier `f`f x0, then Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f is continuous at Unknown identifier `x0`x0. (b) If Unknown identifier `f`f is continuous on Unknown identifier `X`X and Unknown identifier `g`g is continuous on Unknown identifier `Y`Y, then Unknown identifier `g`sorry ∘ sorry : ?m.1 → ?m.3g ∘ Unknown identifier `f`f is continuous on Unknown identifier `X`X.

theorem continuity_preserved_by_composition {X Y Z : Type*} [MetricSpace X] [MetricSpace Y] [MetricSpace Z] : (∀ (f : X → Y) (g : Y → Z) (x0 : X), IsContinuousAt f x0 → IsContinuousAt g (f x0) → IsContinuousAt (fun x => g (f x)) x0) ∧ (∀ (f : X → Y) (g : Y → Z), IsContinuous f → IsContinuous g → IsContinuous (fun x => g (f x))) := by constructor · intro f g x0 hf hg have hf' : ContinuousAt f x0 := by simpa [IsContinuousAt] using hf have hg' : ContinuousAt g (f x0) := by simpa [IsContinuousAt] using hg have hcomp : ContinuousAt (fun x => g (f x)) x0 := hg'.comp hf' simpa [IsContinuousAt] using hcomp · Try this: intro f g hf hg x0intro f g hf hg intro x0 have hf' : ContinuousAt f x0 := by have hfAt : IsContinuousAt f x0 := hf x0 simpa [IsContinuousAt] using hfAt have hg' : ContinuousAt g (f x0) := by have hgAt : IsContinuousAt g (f x0) := hg (f x0) simpa [IsContinuousAt] using hgAt have hcomp : ContinuousAt (fun x => g (f x)) x0 := hg'.comp hf' simpa [IsContinuousAt] using hcomp

Proposition 2.4: Let be a function between metric spaces, and let Unknown identifier `E`sorry ⊆ sorry : PropE ⊆ Unknown identifier `Y`Y contain the image of Unknown identifier `f`f. Let be the codomain restriction of Unknown identifier `f`f with Unknown identifier `g`sorry = sorry : Propg x = Unknown identifier `f`f x. Then for any Unknown identifier `x0`sorry ∈ sorry : Propx0 ∈ Unknown identifier `X`X, Unknown identifier `f`f is continuous at Unknown identifier `x0`x0 iff Unknown identifier `g`g is continuous at Unknown identifier `x0`x0.

theorem continuousAt_codomainRestrict_iff {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (E : Set Y) (hE : ∀ x, f x ∈ E) (x0 : X) : IsContinuousAt f x0 ↔ IsContinuousAt (Set.codRestrict f E hE) x0 := by try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [IsContinuousAt] using (continuousAt_codRestrict_iff (f := f) (t := E) (h1 := hE) (x := x0)).symm
end Section01end Chap02