Changes
13 changed files (+0/-2224)
-
-
@@ -1,227 +0,0 @@import Mathlib.Algebra.BigOperators.Ring import Mathlib.Data.Real.Basic noncomputable section @[ext] structure Point where x : ℝ y : ℝ z : ℝ #check Point.ext example (a b : Point) (hx : a.x = b.x) (hy : a.y = b.y) (hz : a.z = b.z) : a = b := by ext repeat' assumption def myPoint1 : Point where x := 2 y := -1 z := 4 def myPoint2 : Point := ⟨2, -1, 4⟩ def myPoint3 := Point.mk 2 (-1) 4 structure Point' where build :: x : ℝ y : ℝ z : ℝ #check Point'.build 2 (-1) 4 namespace Point def add (a b : Point) : Point := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩ def add' (a b : Point) : Point where x := a.x + b.x y := a.y + b.y z := a.z + b.z #check add myPoint1 myPoint2 #check myPoint1.add myPoint2 end Point #check Point.add myPoint1 myPoint2 #check myPoint1.add myPoint2 namespace Point protected theorem add_comm (a b : Point) : add a b = add b a := by rw [add, add] ext <;> dsimp repeat' apply add_comm example (a b : Point) : add a b = add b a := by simp [add, add_comm] theorem add_x (a b : Point) : (a.add b).x = a.x + b.x := rfl def addAlt : Point → Point → Point | Point.mk x₁ y₁ z₁, Point.mk x₂ y₂ z₂ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩ def addAlt' : Point → Point → Point | ⟨x₁, y₁, z₁⟩, ⟨x₂, y₂, z₂⟩ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩ theorem addAlt_x (a b : Point) : (a.addAlt b).x = a.x + b.x := by cases a cases b rfl theorem addAlt_comm (a b : Point) : addAlt a b = addAlt b a := by rcases a with ⟨xa, ya, za⟩ rcases b with ⟨xb, yb, zb⟩ rw [addAlt, addAlt] ext <;> dsimp apply add_comm repeat' apply add_comm example (a b : Point) : addAlt a b = addAlt b a := by rcases a with ⟨xa, ya, za⟩ rcases b with ⟨xb, yb, zb⟩ simp [addAlt, add_comm] example : ∀ a b : Point, addAlt a b = addAlt b a := by rintro ⟨xa, ya, za⟩ ⟨xb, yb, zb⟩ simp [addAlt, add_comm] example : ∀ a b : Point, add a b = add b a := fun ⟨xa, ya, za⟩ ⟨xb, yb, zb⟩ => by simp [add, add_comm] protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c) := by sorry def smul (r : ℝ) (a : Point) : Point := sorry theorem smul_distrib (r : ℝ) (a b : Point) : (smul r a).add (smul r b) = smul r (a.add b) := by sorry end Point structure StandardTwoSimplex where x : ℝ y : ℝ z : ℝ x_nonneg : 0 ≤ x y_nonneg : 0 ≤ y z_nonneg : 0 ≤ z sum_eq : x + y + z = 1 namespace StandardTwoSimplex def swapXy (a : StandardTwoSimplex) : StandardTwoSimplex where x := a.y y := a.x z := a.z x_nonneg := a.y_nonneg y_nonneg := a.x_nonneg z_nonneg := a.z_nonneg sum_eq := by rw [add_comm a.y a.x, a.sum_eq] noncomputable section def midpoint (a b : StandardTwoSimplex) : StandardTwoSimplex where x := (a.x + b.x) / 2 y := (a.y + b.y) / 2 z := (a.z + b.z) / 2 x_nonneg := div_nonneg (add_nonneg a.x_nonneg b.x_nonneg) (by norm_num) y_nonneg := div_nonneg (add_nonneg a.y_nonneg b.y_nonneg) (by norm_num) z_nonneg := div_nonneg (add_nonneg a.z_nonneg b.z_nonneg) (by norm_num) sum_eq := by field_simp; linarith [a.sum_eq, b.sum_eq] def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : StandardTwoSimplex) : StandardTwoSimplex where sorry end end StandardTwoSimplex open BigOperators structure StandardSimplex (n : ℕ) where V : Fin n → ℝ NonNeg : ∀ i : Fin n, 0 ≤ V i sum_eq_one : (∑ i, V i) = 1 namespace StandardSimplex def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n where V i := (a.V i + b.V i) / 2 NonNeg := by intro i apply div_nonneg · linarith [a.NonNeg i, b.NonNeg i] norm_num sum_eq_one := by simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib, a.sum_eq_one, b.sum_eq_one] field_simp end StandardSimplex structure IsLinear (f : ℝ → ℝ) where is_additive : ∀ x y, f (x + y) = f x + f y preserves_mul : ∀ x c, f (c * x) = c * f x section variable (f : ℝ → ℝ) (linf : IsLinear f) #check linf.is_additive #check linf.preserves_mul end def Point'' := ℝ × ℝ × ℝ def IsLinear' (f : ℝ → ℝ) := (∀ x y, f (x + y) = f x + f y) ∧ ∀ x c, f (c * x) = c * f x def PReal := { y : ℝ // 0 < y } section variable (x : PReal) #check x.val #check x.property #check x.1 #check x.2 end def StandardTwoSimplex' := { p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 } def StandardSimplex' (n : ℕ) := { v : Fin n → ℝ // (∀ i : Fin n, 0 ≤ v i) ∧ (∑ i, v i) = 1 } def StdSimplex := Σ n : ℕ, StandardSimplex n section variable (s : StdSimplex) #check s.fst #check s.snd #check s.1 #check s.2 end
-
-
-
@@ -1,172 +0,0 @@import Mathlib.Data.Real.Basic structure Group₁ (α : Type _) where mul : α → α → α one : α inv : α → α mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z) mul_one : ∀ x : α, mul x one = x one_mul : ∀ x : α, mul one x = x mul_left_inv : ∀ x : α, mul (inv x) x = one structure Group₁Cat where α : Type _ str : Group₁ α section variable (α β γ : Type _) variable (f : α ≃ β) (g : β ≃ γ) #check Equiv α β #check (f.toFun : α → β) #check (f.invFun : β → α) #check (f.right_inv : ∀ x : β, f (f.invFun x) = x) #check (f.left_inv : ∀ x : α, f.invFun (f x) = x) #check (Equiv.refl α : α ≃ α) #check (f.symm : β ≃ α) #check (f.trans g : α ≃ γ) example (x : α) : (f.trans g).toFun x = g.toFun (f.toFun x) := rfl example (x : α) : (f.trans g) x = g (f x) := rfl example : (f.trans g : α → γ) = g ∘ f := rfl end example (α : Type _) : Equiv.Perm α = (α ≃ α) := rfl def permGroup {α : Type _} : Group₁ (Equiv.Perm α) where mul f g := Equiv.trans g f one := Equiv.refl α inv := Equiv.symm mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm one_mul := Equiv.trans_refl mul_one := Equiv.refl_trans mul_left_inv := Equiv.self_trans_symm structure AddGroup₁ (α : Type _) where (add : α → α → α) -- fill in the rest @[ext] structure Point where x : ℝ y : ℝ z : ℝ namespace Point def add (a b : Point) : Point := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩ def neg (a : point) : point := sorry def zero : point := sorry def add_group_point : add_group₁ point := sorry end Point section variable {α : Type _} (f g : Equiv.Perm α) (n : ℕ) #check f * g #check mul_assoc f g g⁻¹ -- group power, defined for any group #check g ^ n example : f * g * g⁻¹ = f := by rw [mul_assoc, mul_right_inv, mul_one] example : f * g * g⁻¹ = f := mul_inv_cancel_right f g example {α : Type _} (f g : Equiv.Perm α) : g.symm.trans (g.trans f) = f := mul_inv_cancel_right f g end class Group₂ (α : Type _) where mul : α → α → α one : α inv : α → α mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z) mul_one : ∀ x : α, mul x one = x one_mul : ∀ x : α, mul one x = x mul_left_inv : ∀ x : α, mul (inv x) x = one instance {α : Type _} : Group₂ (Equiv.Perm α) where mul f g := Equiv.trans g f one := Equiv.refl α inv := Equiv.symm mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm one_mul := Equiv.trans_refl mul_one := Equiv.refl_trans mul_left_inv := Equiv.self_trans_symm #check @Group₂.mul def mySquare {α : Type _} [Group₂ α] (x : α) := Group₂.mul x x #check @mySquare section variable {β : Type _} (f g : Equiv.Perm β) example : Group₂.mul f g = g.trans f := rfl example : mySquare f = f.trans f := rfl end instance : Inhabited Point where default := ⟨0, 0, 0⟩ #check (default : Point) example : ([] : List Point).headI = default := rfl instance : Add Point where add := Point.add section variable (x y : Point) #check x + y example : x + y = Point.add x y := rfl end instance hasMulGroup₂ {α : Type _} [Group₂ α] : Mul α := ⟨Group₂.mul⟩ instance hasOneGroup₂ {α : Type _} [Group₂ α] : One α := ⟨Group₂.one⟩ instance hasInvGroup₂ {α : Type _} [Group₂ α] : Inv α := ⟨Group₂.inv⟩ section variable {α : Type _} (f g : Equiv.Perm α) #check f * 1 * g⁻¹ def foo : f * 1 * g⁻¹ = g.symm.trans ((Equiv.refl α).trans f) := rfl end class AddGroup₂ (α : Type _) where add : α → α → α -- fill in the rest
-
-
-
@@ -1,271 +0,0 @@import Mathlib.Data.Int.Basic import Mathlib.Algebra.EuclideanDomain.Basic import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.Tactic @[ext] structure gaussInt where re : ℤ im : ℤ namespace gaussInt instance : Zero gaussInt := ⟨⟨0, 0⟩⟩ instance : One gaussInt := ⟨⟨1, 0⟩⟩ instance : Add gaussInt := ⟨fun x y => ⟨x.re + y.re, x.im + y.im⟩⟩ instance : Neg gaussInt := ⟨fun x => ⟨-x.re, -x.im⟩⟩ instance : Mul gaussInt := ⟨fun x y => ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩⟩ theorem zero_def : (0 : gaussInt) = ⟨0, 0⟩ := rfl theorem one_def : (1 : gaussInt) = ⟨1, 0⟩ := rfl theorem add_def (x y : gaussInt) : x + y = ⟨x.re + y.re, x.im + y.im⟩ := rfl theorem neg_def (x : gaussInt) : -x = ⟨-x.re, -x.im⟩ := rfl theorem mul_def (x y : gaussInt) : x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := rfl @[simp] theorem zero_re : (0 : gaussInt).re = 0 := rfl @[simp] theorem zero_im : (0 : gaussInt).im = 0 := rfl @[simp] theorem one_re : (1 : gaussInt).re = 1 := rfl @[simp] theorem one_im : (1 : gaussInt).im = 0 := rfl @[simp] theorem add_re (x y : gaussInt) : (x + y).re = x.re + y.re := rfl @[simp] theorem add_im (x y : gaussInt) : (x + y).im = x.im + y.im := rfl @[simp] theorem neg_re (x : gaussInt) : (-x).re = -x.re := rfl @[simp] theorem neg_im (x : gaussInt) : (-x).im = -x.im := rfl @[simp] theorem mul_re (x y : gaussInt) : (x * y).re = x.re * y.re - x.im * y.im := rfl @[simp] theorem mul_im (x y : gaussInt) : (x * y).im = x.re * y.im + x.im * y.re := rfl instance instCommRing : CommRing gaussInt where zero := 0 one := 1 add := (· + ·) neg x := -x mul := (· * ·) add_assoc := by intros ext <;> simp <;> ring zero_add := by intros ext <;> simp add_zero := by intros ext <;> simp add_left_neg := by intros ext <;> simp add_comm := by intros ext <;> simp <;> ring mul_assoc := by intros ext <;> simp <;> ring one_mul := by intros ext <;> simp mul_one := by intros ext <;> simp left_distrib := by intros ext <;> simp <;> ring right_distrib := by intros ext <;> simp <;> ring mul_comm := by intros ext <;> simp <;> ring zero_mul := sorry mul_zero := sorry instance : Nontrivial gaussInt := by use 0, 1 rw [Ne, gaussInt.ext_iff] simp end gaussInt example (a b : ℤ) : a = b * (a / b) + a % b := Eq.symm <| Int.ediv_add_emod a b example (a b : ℤ) : b ≠ 0 → 0 ≤ a % b := Int.emod_nonneg a example (a b : ℤ) : b ≠ 0 → a % b < |b| := Int.emod_lt a namespace Int def div' (a b : ℤ) := (a + b / 2) / b def mod' (a b : ℤ) := (a + b / 2) % b - b / 2 theorem div'_add_mod' (a b : ℤ) : b * div' a b + mod' a b = a := by rw [div', mod'] linarith [Int.ediv_add_emod (a + b / 2) b] theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : |mod' a b| ≤ b / 2 := by rw [mod', abs_le] constructor · linarith [Int.emod_nonneg (a + b / 2) h.ne'] have := Int.emod_lt_of_pos (a + b / 2) h have := Int.ediv_add_emod b 2 have := Int.emod_lt_of_pos b zero_lt_two revert this; intro this -- FIXME, this should not be needed linarith theorem mod'_eq (a b : ℤ) : mod' a b = a - b * div' a b := by linarith [div'_add_mod' a b] end Int theorem sq_add_sq_eq_zero {α : Type _} [LinearOrderedRing α] (x y : α) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by sorry namespace gaussInt def norm (x : gaussInt) := x.re ^ 2 + x.im ^ 2 @[simp] theorem norm_nonneg (x : gaussInt) : 0 ≤ norm x := by sorry theorem norm_eq_zero (x : gaussInt) : norm x = 0 ↔ x = 0 := by sorry theorem norm_pos (x : gaussInt) : 0 < norm x ↔ x ≠ 0 := by sorry theorem norm_mul (x y : gaussInt) : norm (x * y) = norm x * norm y := by sorry def conj (x : gaussInt) : gaussInt := ⟨x.re, -x.im⟩ @[simp] theorem conj_re (x : gaussInt) : (conj x).re = x.re := rfl @[simp] theorem conj_im (x : gaussInt) : (conj x).im = -x.im := rfl theorem norm_conj (x : gaussInt) : norm (conj x) = norm x := by simp [norm] instance : Div gaussInt := ⟨fun x y => ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩⟩ instance : Mod gaussInt := ⟨fun x y => x - y * (x / y)⟩ theorem div_def (x y : gaussInt) : x / y = ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩ := rfl theorem mod_def (x y : gaussInt) : x % y = x - y * (x / y) := rfl theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : (x % y).norm < y.norm := by have norm_y_pos : 0 < norm y := by rwa [norm_pos] have : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩ := by rw [mod_def, sub_mul, Int.mod'_eq, Int.mod'_eq, sub_eq_add_neg, div_def, norm] ext <;> simp <;> ring have : norm (x % y) * norm y ≤ norm y / 2 * norm y := by conv => lhs rw [← norm_conj y, ← norm_mul, this, norm] simp trans 2 * (y.norm / 2) ^ 2 · rw [two_mul] apply add_le_add <;> · rw [sq_le_sq] apply le_trans (Int.abs_mod'_le _ _ norm_y_pos) apply le_abs_self rw [pow_two, ← mul_assoc, mul_comm, mul_comm (2 : ℤ)] apply mul_le_mul_of_nonneg_left · apply Int.ediv_mul_le norm_num apply Int.ediv_nonneg (norm_nonneg y) norm_num have : norm (x % y) ≤ norm y / 2 := le_of_mul_le_mul_right this norm_y_pos apply lt_of_le_of_lt this apply Int.ediv_lt_of_lt_mul · norm_num linarith theorem coe_natAbs_norm (x : gaussInt) : (x.norm.natAbs : ℤ) = x.norm := Int.natAbs_of_nonneg (norm_nonneg _) theorem natAbs_norm_mod_lt (x y : gaussInt) (hy : y ≠ 0) : (x % y).norm.natAbs < y.norm.natAbs := by apply Int.ofNat_lt.1 simp only [Int.coe_natAbs, abs_of_nonneg, norm_nonneg] apply norm_mod_lt x hy theorem not_norm_mul_left_lt_norm (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : ¬(norm (x * y)).natAbs < (norm x).natAbs := by apply not_lt_of_ge rw [norm_mul, Int.natAbs_mul] apply le_mul_of_one_le_right (Nat.zero_le _) apply Int.ofNat_le.1 rw [coe_natAbs_norm] exact Int.add_one_le_of_lt ((norm_pos _).mpr hy) instance : EuclideanDomain gaussInt := { gaussInt.instCommRing with quotient := (· / ·) remainder := (· % ·) quotient_mul_add_remainder_eq := fun x y => by simp only; rw [mod_def, add_comm, sub_add_cancel] quotient_zero := fun x => by simp [div_def, norm, Int.div'] rfl r := Measure (Int.natAbs ∘ norm) r_wellFounded := (measure (Int.natAbs ∘ norm)).2 remainder_lt := natAbs_norm_mod_lt mul_left_not_lt := not_norm_mul_left_lt_norm } example (x : gaussInt) : Irreducible x ↔ Prime x := PrincipalIdealRing.irreducible_iff_prime end gaussInt
-
-
-
@@ -1,96 +0,0 @@import Mathlib.Algebra.BigOperators.Ring import Mathlib.Data.Real.Basic noncomputable section @[ext] structure Point where x : ℝ y : ℝ z : ℝ namespace Point def add (a b : Point) : Point := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩ protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c) := by simp [add, add_assoc] def smul (r : ℝ) (a : Point) : Point := ⟨r * a.x, r * a.y, r * a.z⟩ theorem smul_distrib (r : ℝ) (a b : Point) : (smul r a).add (smul r b) = smul r (a.add b) := by simp [add, smul, mul_add] end Point structure StandardTwoSimplex where x : ℝ y : ℝ z : ℝ x_nonneg : 0 ≤ x y_nonneg : 0 ≤ y z_nonneg : 0 ≤ z sum_eq : x + y + z = 1 namespace StandardTwoSimplex noncomputable section def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : StandardTwoSimplex) : StandardTwoSimplex where x := lambda * a.x + (1 - lambda) * b.x y := lambda * a.y + (1 - lambda) * b.y z := lambda * a.z + (1 - lambda) * b.z x_nonneg := add_nonneg (mul_nonneg lambda_nonneg a.x_nonneg) (mul_nonneg (by linarith) b.x_nonneg) y_nonneg := add_nonneg (mul_nonneg lambda_nonneg a.y_nonneg) (mul_nonneg (by linarith) b.y_nonneg) z_nonneg := add_nonneg (mul_nonneg lambda_nonneg a.z_nonneg) (mul_nonneg (by linarith) b.z_nonneg) sum_eq := by trans (a.x + a.y + a.z) * lambda + (b.x + b.y + b.z) * (1 - lambda) · ring simp [a.sum_eq, b.sum_eq] end end StandardTwoSimplex open BigOperators structure StandardSimplex (n : ℕ) where V : Fin n → ℝ NonNeg : ∀ i : Fin n, 0 ≤ V i sum_eq_one : (∑ i, V i) = 1 namespace StandardSimplex def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n where V i := (a.V i + b.V i) / 2 NonNeg := by intro i apply div_nonneg · linarith [a.NonNeg i, b.NonNeg i] norm_num sum_eq_one := by simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib, a.sum_eq_one, b.sum_eq_one] field_simp end StandardSimplex namespace StandardSimplex def weightedAverage {n : ℕ} (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : StandardSimplex n) : StandardSimplex n where V i := lambda * a.V i + (1 - lambda) * b.V i NonNeg i := add_nonneg (mul_nonneg lambda_nonneg (a.NonNeg i)) (mul_nonneg (by linarith) (b.NonNeg i)) sum_eq_one := by trans (lambda * ∑ i, a.V i) + (1 - lambda) * ∑ i, b.V i · rw [Finset.sum_add_distrib, Finset.mul_sum, Finset.mul_sum] simp [a.sum_eq_one, b.sum_eq_one] end StandardSimplex
-
-
-
@@ -1,73 +0,0 @@import Mathlib.Data.Real.Basic structure AddGroup₁ (α : Type _) where add : α → α → α zero : α neg : α → α add_assoc : ∀ x y z : α, add (add x y) z = add x (add y z) add_zero : ∀ x : α, add x zero = x zero_add : ∀ x : α, add x zero = x add_left_neg : ∀ x : α, add (neg x) x = zero @[ext] structure Point where x : ℝ y : ℝ z : ℝ namespace Point def add (a b : Point) : Point := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩ def neg (a : Point) : Point := ⟨-a.x, -a.y, -a.z⟩ def zero : Point := ⟨0, 0, 0⟩ def addGroupPoint : AddGroup₁ Point where add := Point.add zero := Point.zero neg := Point.neg add_assoc := by simp [Point.add, add_assoc] add_zero := by simp [Point.add, Point.zero] zero_add := by simp [Point.add, Point.zero] add_left_neg := by simp [Point.add, Point.neg, Point.zero] end Point class AddGroup₂ (α : Type _) where add : α → α → α zero : α neg : α → α add_assoc : ∀ x y z : α, add (add x y) z = add x (add y z) add_zero : ∀ x : α, add x zero = x zero_add : ∀ x : α, add x zero = x add_left_neg : ∀ x : α, add (neg x) x = zero instance hasAddAddGroup₂ {α : Type _} [AddGroup₂ α] : Add α := ⟨AddGroup₂.add⟩ instance hasZeroAddGroup₂ {α : Type _} [AddGroup₂ α] : Zero α := ⟨AddGroup₂.zero⟩ instance hasNegAddGroup₂ {α : Type _} [AddGroup₂ α] : Neg α := ⟨AddGroup₂.neg⟩ instance : AddGroup₂ Point where add := Point.add zero := Point.zero neg := Point.neg add_assoc := by simp [Point.add, add_assoc] add_zero := by simp [Point.add, Point.zero] zero_add := by simp [Point.add, Point.zero] add_left_neg := by simp [Point.add, Point.neg, Point.zero] section variable (x y : Point) #check x + -y + 0 end
-
-
-
@@ -1,285 +0,0 @@import Mathlib.Data.Int.Basic import Mathlib.Algebra.EuclideanDomain.Basic import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.Tactic @[ext] structure gaussInt where re : ℤ im : ℤ namespace gaussInt instance : Zero gaussInt := ⟨⟨0, 0⟩⟩ instance : One gaussInt := ⟨⟨1, 0⟩⟩ instance : Add gaussInt := ⟨fun x y => ⟨x.re + y.re, x.im + y.im⟩⟩ instance : Neg gaussInt := ⟨fun x => ⟨-x.re, -x.im⟩⟩ instance : Mul gaussInt := ⟨fun x y => ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩⟩ theorem zero_def : (0 : gaussInt) = ⟨0, 0⟩ := rfl theorem one_def : (1 : gaussInt) = ⟨1, 0⟩ := rfl theorem add_def (x y : gaussInt) : x + y = ⟨x.re + y.re, x.im + y.im⟩ := rfl theorem neg_def (x : gaussInt) : -x = ⟨-x.re, -x.im⟩ := rfl theorem mul_def (x y : gaussInt) : x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := rfl @[simp] theorem zero_re : (0 : gaussInt).re = 0 := rfl @[simp] theorem zero_im : (0 : gaussInt).im = 0 := rfl @[simp] theorem one_re : (1 : gaussInt).re = 1 := rfl @[simp] theorem one_im : (1 : gaussInt).im = 0 := rfl @[simp] theorem add_re (x y : gaussInt) : (x + y).re = x.re + y.re := rfl @[simp] theorem add_im (x y : gaussInt) : (x + y).im = x.im + y.im := rfl @[simp] theorem neg_re (x : gaussInt) : (-x).re = -x.re := rfl @[simp] theorem neg_im (x : gaussInt) : (-x).im = -x.im := rfl @[simp] theorem mul_re (x y : gaussInt) : (x * y).re = x.re * y.re - x.im * y.im := rfl @[simp] theorem mul_im (x y : gaussInt) : (x * y).im = x.re * y.im + x.im * y.re := rfl instance instCommRing : CommRing gaussInt where zero := 0 one := 1 add := (· + ·) neg x := -x mul := (· * ·) add_assoc := by intros ext <;> simp <;> ring zero_add := by intros ext <;> simp add_zero := by intros ext <;> simp add_left_neg := by intros ext <;> simp add_comm := by intros ext <;> simp <;> ring mul_assoc := by intros ext <;> simp <;> ring one_mul := by intros ext <;> simp mul_one := by intros ext <;> simp left_distrib := by intros ext <;> simp <;> ring right_distrib := by intros ext <;> simp <;> ring mul_comm := by intros ext <;> simp <;> ring zero_mul := sorry mul_zero := sorry instance : Nontrivial gaussInt := by use 0, 1 rw [Ne, gaussInt.ext_iff] simp end gaussInt namespace Int def div' (a b : ℤ) := (a + b / 2) / b def mod' (a b : ℤ) := (a + b / 2) % b - b / 2 theorem div'_add_mod' (a b : ℤ) : b * div' a b + mod' a b = a := by rw [div', mod'] linarith [Int.ediv_add_emod (a + b / 2) b] theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : abs (mod' a b) ≤ b / 2 := by rw [mod', abs_le] constructor · linarith [Int.emod_nonneg (a + b / 2) h.ne'] have := Int.emod_lt_of_pos (a + b / 2) h have := Int.ediv_add_emod b 2 have := Int.emod_lt_of_pos b zero_lt_two revert this; intro this -- FIXME, this should not be needed linarith theorem mod'_eq (a b : ℤ) : mod' a b = a - b * div' a b := by linarith [div'_add_mod' a b] end Int private theorem aux {α : Type _} [LinearOrderedRing α] {x y : α} (h : x ^ 2 + y ^ 2 = 0) : x = 0 := haveI h' : x ^ 2 = 0 := by apply le_antisymm _ (sq_nonneg x) rw [← h] apply le_add_of_nonneg_right (sq_nonneg y) pow_eq_zero h' theorem sq_add_sq_eq_zero {α : Type _} [LinearOrderedRing α] (x y : α) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by constructor · intro h constructor · exact aux h rw [add_comm] at h exact aux h rintro ⟨rfl, rfl⟩ norm_num namespace gaussInt def norm (x : gaussInt) := x.re ^ 2 + x.im ^ 2 @[simp] theorem norm_nonneg (x : gaussInt) : 0 ≤ norm x := by apply add_nonneg <;> apply sq_nonneg theorem norm_eq_zero (x : gaussInt) : norm x = 0 ↔ x = 0 := by rw [norm, sq_add_sq_eq_zero, gaussInt.ext_iff] rfl theorem norm_pos (x : gaussInt) : 0 < norm x ↔ x ≠ 0 := by rw [lt_iff_le_and_ne, ne_comm, Ne, norm_eq_zero] simp [norm_nonneg] theorem norm_mul (x y : gaussInt) : norm (x * y) = norm x * norm y := by simp [norm] ring def conj (x : gaussInt) : gaussInt := ⟨x.re, -x.im⟩ @[simp] theorem conj_re (x : gaussInt) : (conj x).re = x.re := rfl @[simp] theorem conj_im (x : gaussInt) : (conj x).im = -x.im := rfl theorem norm_conj (x : gaussInt) : norm (conj x) = norm x := by simp [norm] instance : Div gaussInt := ⟨fun x y => ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩⟩ instance : Mod gaussInt := ⟨fun x y => x - y * (x / y)⟩ theorem div_def (x y : gaussInt) : x / y = ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩ := rfl theorem mod_def (x y : gaussInt) : x % y = x - y * (x / y) := rfl theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : (x % y).norm < y.norm := by have norm_y_pos : 0 < norm y := by rwa [norm_pos] have : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩ := by rw [mod_def, sub_mul, Int.mod'_eq, Int.mod'_eq, sub_eq_add_neg, div_def, norm] ext <;> simp <;> ring have : norm (x % y) * norm y ≤ norm y / 2 * norm y := by conv => lhs rw [← norm_conj y, ← norm_mul, this, norm] simp trans 2 * (y.norm / 2) ^ 2 · rw [two_mul] apply add_le_add <;> · rw [sq_le_sq] apply le_trans (Int.abs_mod'_le _ _ norm_y_pos) apply le_abs_self rw [pow_two, ← mul_assoc, mul_comm, mul_comm (2 : ℤ)] apply mul_le_mul_of_nonneg_left · apply Int.ediv_mul_le norm_num apply Int.ediv_nonneg (norm_nonneg y) norm_num have : norm (x % y) ≤ norm y / 2 := le_of_mul_le_mul_right this norm_y_pos apply lt_of_le_of_lt this apply Int.ediv_lt_of_lt_mul · norm_num linarith theorem coe_natAbs_norm (x : gaussInt) : (x.norm.natAbs : ℤ) = x.norm := Int.natAbs_of_nonneg (norm_nonneg _) theorem natAbs_norm_mod_lt (x y : gaussInt) (hy : y ≠ 0) : (x % y).norm.natAbs < y.norm.natAbs := by apply Int.ofNat_lt.1 simp only [Int.coe_natAbs, abs_of_nonneg, norm_nonneg] apply norm_mod_lt x hy theorem not_norm_mul_left_lt_norm (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : ¬(norm (x * y)).natAbs < (norm x).natAbs := by apply not_lt_of_ge rw [norm_mul, Int.natAbs_mul] apply le_mul_of_one_le_right (Nat.zero_le _) apply Int.ofNat_le.1 rw [coe_natAbs_norm] exact Int.add_one_le_of_lt ((norm_pos _).mpr hy) instance : EuclideanDomain gaussInt := { gaussInt.instCommRing with quotient := (· / ·) remainder := (· % ·) quotient_mul_add_remainder_eq := fun x y => by simp only; rw [mod_def, add_comm, sub_add_cancel] quotient_zero := fun x => by simp [div_def, norm, Int.div'] rfl r := Measure (Int.natAbs ∘ norm) r_wellFounded := (measure (Int.natAbs ∘ norm)).2 remainder_lt := natAbs_norm_mod_lt mul_left_not_lt := not_norm_mul_left_lt_norm } example (x : gaussInt) : Irreducible x ↔ Prime x := PrincipalIdealRing.irreducible_iff_prime end gaussInt
-
-
MIL/C07_Topology/S01_Filters.lean (deleted)
-
@@ -1,110 +0,0 @@import Mathlib.Topology.Instances.Real open Set Filter Topology def principal {α : Type _} (s : Set α) : Filter α where sets := { t | s ⊆ t } univ_sets := sorry sets_of_superset := sorry inter_sets := sorry example : Filter ℕ := { sets := { s | ∃ a, ∀ b, a ≤ b → b ∈ s } univ_sets := sorry sets_of_superset := sorry inter_sets := sorry } def Tendsto₁ {X Y : Type _} (f : X → Y) (F : Filter X) (G : Filter Y) := ∀ V ∈ G, f ⁻¹' V ∈ F def Tendsto₂ {X Y : Type _} (f : X → Y) (F : Filter X) (G : Filter Y) := map f F ≤ G example {X Y : Type _} (f : X → Y) (F : Filter X) (G : Filter Y) : Tendsto₂ f F G ↔ Tendsto₁ f F G := Iff.rfl #check (@Filter.map_mono : ∀ {α β} {m : α → β}, Monotone (map m)) #check (@Filter.map_map : ∀ {α β γ} {f : Filter α} {m : α → β} {m' : β → γ}, map m' (map m f) = map (m' ∘ m) f) example {X Y Z : Type _} {F : Filter X} {G : Filter Y} {H : Filter Z} {f : X → Y} {g : Y → Z} (hf : Tendsto₁ f F G) (hg : Tendsto₁ g G H) : Tendsto₁ (g ∘ f) F H := sorry variable (f : ℝ → ℝ) (x₀ y₀ : ℝ) #check comap ((↑) : ℚ → ℝ) (𝓝 x₀) #check Tendsto (f ∘ (↑)) (comap ((↑) : ℚ → ℝ) (𝓝 x₀)) (𝓝 y₀) section variable {α β γ : Type _} (F : Filter α) {m : γ → β} {n : β → α} #check (comap_comap : comap m (comap n F) = comap (n ∘ m) F) end example : 𝓝 (x₀, y₀) = 𝓝 x₀ ×ᶠ 𝓝 y₀ := nhds_prod_eq #check le_inf_iff example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) : Tendsto f atTop (𝓝 (x₀, y₀)) ↔ Tendsto (Prod.fst ∘ f) atTop (𝓝 x₀) ∧ Tendsto (Prod.snd ∘ f) atTop (𝓝 y₀) := sorry example (x₀ : ℝ) : HasBasis (𝓝 x₀) (fun ε : ℝ => 0 < ε) fun ε => Ioo (x₀ - ε) (x₀ + ε) := nhds_basis_Ioo_pos x₀ example (u : ℕ → ℝ) (x₀ : ℝ) : Tendsto u atTop (𝓝 x₀) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ∈ Ioo (x₀ - ε) (x₀ + ε) := by have : atTop.HasBasis (fun n : ℕ => True) Ici := atTop_basis rw [this.tendsto_iff (nhds_basis_Ioo_pos x₀)] simp example (P Q : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n) : ∀ᶠ n in atTop, P n ∧ Q n := hP.and hQ example (u v : ℕ → ℝ) (h : ∀ᶠ n in atTop, u n = v n) (x₀ : ℝ) : Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) := tendsto_congr' h example (u v : ℕ → ℝ) (h : u =ᶠ[atTop] v) (x₀ : ℝ) : Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) := tendsto_congr' h #check @eventually_of_forall #check @Eventually.mono #check @Eventually.and example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n) (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by apply (hP.and (hQ.and hR)).mono rintro n ⟨h, h', h''⟩ exact h'' ⟨h, h'⟩ example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n) (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by filter_upwards [hP, hQ, hR] intro n h h' h'' exact h'' ⟨h, h'⟩ #check mem_closure_iff_clusterPt #check le_principal_iff #check neBot_of_le example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x)) (huM : ∀ᶠ n in atTop, u n ∈ M) : x ∈ closure M := sorry
-
-
MIL/C07_Topology/S02_Metric_Spaces.lean (deleted)
-
@@ -1,200 +0,0 @@import Mathlib.Topology.Instances.Real import Mathlib.Analysis.NormedSpace.BanachSteinhaus open Set Filter open Topology Filter variable {X : Type _} [MetricSpace X] (a b c : X) #check (dist a b : ℝ) #check (dist_nonneg : 0 ≤ dist a b) #check (dist_eq_zero : dist a b = 0 ↔ a = b) #check (dist_comm a b : dist a b = dist b a) #check (dist_triangle a b c : dist a c ≤ dist a b + dist b c) -- Note the next three lines are not quoted, their purpose is to make sure those things don't get renamed while we're looking elsewhere. #check EMetricSpace #check PseudoMetricSpace #check PseudoEMetricSpace example {u : ℕ → X} {a : X} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := Metric.tendsto_atTop example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} : Continuous f ↔ ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := Metric.continuous_iff example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := by continuity example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := continuous_dist.comp ((hf.comp continuous_fst).prod_mk (hf.comp continuous_snd)) example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := by apply Continuous.dist exact hf.comp continuous_fst exact hf.comp continuous_snd example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := (hf.comp continuous_fst).dist (hf.comp continuous_snd) example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := hf.fst'.dist hf.snd' example {f : ℝ → X} (hf : Continuous f) : Continuous fun x : ℝ => f (x ^ 2 + x) := sorry example {X Y : Type _} [MetricSpace X] [MetricSpace Y] (f : X → Y) (a : X) : ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x}, dist x a < δ → dist (f x) (f a) < ε := Metric.continuousAt_iff variable (r : ℝ) example : Metric.ball a r = { b | dist b a < r } := rfl example : Metric.closedBall a r = { b | dist b a ≤ r } := rfl example (hr : 0 < r) : a ∈ Metric.ball a r := Metric.mem_ball_self hr example (hr : 0 ≤ r) : a ∈ Metric.closedBall a r := Metric.mem_closedBall_self hr example (s : Set X) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s := Metric.isOpen_iff example {s : Set X} : IsClosed s ↔ IsOpen (sᶜ) := isOpen_compl_iff.symm example {s : Set X} (hs : IsClosed s) {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) (hus : ∀ n, u n ∈ s) : a ∈ s := hs.mem_of_tendsto hu (eventually_of_forall hus) example {s : Set X} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, a ∈ Metric.ball b ε := Metric.mem_closure_iff example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := sorry example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s := Metric.nhds_basis_ball.mem_iff example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.closedBall x ε ⊆ s := Metric.nhds_basis_closedBall.mem_iff example : IsCompact (Set.Icc 0 1 : Set ℝ) := isCompact_Icc example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) := hs.tendsto_subseq hu example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f s) : ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y := hs.exists_forall_le hs' hfs example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f s) : ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x := hs.exists_forall_ge hs' hfs example {s : Set X} (hs : IsCompact s) : IsClosed s := hs.IsClosed example {X : Type _} [MetricSpace X] [CompactSpace X] : IsCompact (univ : Set X) := isCompact_univ #check IsCompact.isClosed example {X : Type _} [MetricSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := Metric.uniformContinuous_iff example {X : Type _} [MetricSpace X] [CompactSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} (hf : Continuous f) : UniformContinuous f := sorry example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := Metric.cauchySeq_iff example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := Metric.cauchySeq_iff' example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete hu open BigOperators open Finset theorem cauchySeq_of_le_geometric_two' {u : ℕ → X} (hu : ∀ n : ℕ, dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : CauchySeq u := by rw [Metric.cauchySeq_iff'] intro ε ε_pos obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε := by sorry use N intro n hn obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn calc dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2) ^ i := sorry _ ≤ 1 / 2 ^ N * 2 := sorry _ < ε := sorry open Metric example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : ∀ n, Dense (f n)) : Dense (⋂ n, f n) := by let B : ℕ → ℝ := fun n => (1 / 2) ^ n have Bpos : ∀ n, 0 < B n sorry /- Translate the density assumption into two functions `center` and `radius` associating to any n, x, δ, δpos a center and a positive radius such that `closed_ball center radius` is included both in `f n` and in `closed_ball x δ`. We can also require `radius ≤ (1/2)^(n+1)`, to ensure we get a Cauchy sequence later. -/ have : ∀ (n : ℕ) (x : X), ∀ δ > 0, ∃ y : X, ∃ r > 0, r ≤ B (n + 1) ∧ closed_ball y r ⊆ closed_ball x δ ∩ f n := by sorry choose! center radius Hpos HB Hball using this intro x rw [mem_closure_iff_nhds_basis nhds_basis_closed_ball] intro ε εpos /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball `closed_ball (c n) (r n)` is included in the previous ball and in `f n`, and such that `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs to all the `f n`. -/ let F : ℕ → X × ℝ := fun n => Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) let c : ℕ → X := fun n => (F n).1 let r : ℕ → ℝ := fun n => (F n).2 have rpos : ∀ n, 0 < r n := by sorry have rB : ∀ n, r n ≤ B n := by sorry have incl : ∀ n, closed_ball (c (n + 1)) (r (n + 1)) ⊆ closed_ball (c n) (r n) ∩ f n := by sorry have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by sorry have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`. rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩ -- this point `y` will be the desired point. We will check that it belongs to all -- `f n` and to `ball x ε`. use y have I : ∀ n, ∀ m ≥ n, closed_ball (c m) (r m) ⊆ closed_ball (c n) (r n) := by sorry have yball : ∀ n, y ∈ closed_ball (c n) (r n) := by sorry sorry
-
-
-
@@ -1,151 +0,0 @@import Mathlib.Topology.Instances.Real import Mathlib.Analysis.NormedSpace.BanachSteinhaus open Set Filter open Topology Filter section variable {X : Type _} [TopologicalSpace X] example : IsOpen (univ : Set X) := isOpen_univ example : IsOpen (∅ : Set X) := isOpen_empty example {ι : Type _} {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋃ i, s i) := isOpen_iUnion hs example {ι : Type _} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋂ i, s i) := isOpen_iInter hs variable {Y : Type _} [TopologicalSpace Y] example {f : X → Y} : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) := continuous_def example {f : X → Y} {x : X} : ContinuousAt f x ↔ map f (𝓝 x) ≤ 𝓝 (f x) := Iff.rfl example {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ U ∈ 𝓝 (f x), ∀ᶠ x in 𝓝 x, f x ∈ U := Iff.rfl example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := mem_nhds_iff example (x : X) : pure x ≤ 𝓝 x := pure_le_nhds x example (x : X) (P : X → Prop) (h : ∀ᶠ y in 𝓝 x, P y) : P x := pure_le_nhds x h example {P : X → Prop} {x : X} (h : ∀ᶠ y in 𝓝 x, P y) : ∀ᶠ y in 𝓝 x, ∀ᶠ z in 𝓝 y, P z := eventually_eventually_nhds.mpr h #check TopologicalSpace.mkOfNhds #check TopologicalSpace.nhds_mkOfNhds example {α : Type _} (n : α → Filter α) (H₀ : ∀ a, pure a ≤ n a) (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x) : ∀ a, ∀ s ∈ n a, ∃ t ∈ n a, t ⊆ s ∧ ∀ a' ∈ t, s ∈ n a' := sorry end -- BOTH. variable {X Y : Type _} example (f : X → Y) : TopologicalSpace X → TopologicalSpace Y := TopologicalSpace.coinduced f example (f : X → Y) : TopologicalSpace Y → TopologicalSpace X := TopologicalSpace.induced f example (f : X → Y) (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) : TopologicalSpace.coinduced f T_X ≤ T_Y ↔ T_X ≤ TopologicalSpace.induced f T_Y := coinduced_le_iff_le_induced #check coinduced_compose #check induced_compose example {T T' : TopologicalSpace X} : T ≤ T' ↔ ∀ s, T'.IsOpen s → T.IsOpen s := Iff.rfl example (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) (f : X → Y) : Continuous f ↔ TopologicalSpace.coinduced f T_X ≤ T_Y := continuous_iff_coinduced_le example {Z : Type _} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z) (g : Y → Z) : @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔ @Continuous X Z T_X T_Z (g ∘ f) := by rw [continuous_iff_coinduced_le, coinduced_compose, continuous_iff_coinduced_le] example (ι : Type _) (X : ι → Type _) (T_X : ∀ i, TopologicalSpace <| X i) : (Pi.topologicalSpace : TopologicalSpace (∀ i, X i)) = ⨅ i, TopologicalSpace.induced (fun x => x i) (T_X i) := rfl example [TopologicalSpace X] [T2Space X] {u : ℕ → X} {a b : X} (ha : Tendsto u atTop (𝓝 a)) (hb : Tendsto u atTop (𝓝 b)) : a = b := tendsto_nhds_unique ha hb example [TopologicalSpace X] [RegularSpace X] (a : X) : (𝓝 a).HasBasis (fun s : Set X => s ∈ 𝓝 a ∧ IsClosed s) id := closed_nhds_basis a example [TopologicalSpace X] {x : X} : (𝓝 x).HasBasis (fun t : Set X => t ∈ 𝓝 x ∧ IsOpen t) id := nhds_basis_opens' x theorem aux {X Y A : Type _} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := sorry example [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] {A : Set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f) (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) <| 𝓝 x) <| 𝓝 c) : ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := sorry #check @HasBasis.tendsto_right_iff example [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] {s : Set X} {a : X} : a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) := mem_closure_iff_seq_limit variable [TopologicalSpace X] example {F : Filter X} {x : X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) := Iff.rfl example {s : Set X} : IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := Iff.rfl example [TopologicalSpace.FirstCountableTopology X] {s : Set X} {u : ℕ → X} (hs : IsCompact s) (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) := hs.tendsto_subseq hu variable [TopologicalSpace Y] example {x : X} {F : Filter X} {G : Filter Y} (H : ClusterPt x F) {f : X → Y} (hfx : ContinuousAt f x) (hf : Tendsto f F G) : ClusterPt (f x) G := ClusterPt.map H hfx hf example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) : IsCompact (f '' s) := by intro F F_ne F_le have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F := by sorry have Hne : (𝓟 s ⊓ comap f F).NeBot := by sorry have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s := inf_le_left sorry example {ι : Type _} {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i := hs.elim_finite_subcover U hUo hsU example [CompactSpace X] : IsCompact (univ : Set X) := isCompact_univ
-
-
-
@@ -1,72 +0,0 @@import Mathlib.Topology.Instances.Real open Set Filter Topology -- In the next example we could use `tauto` in each proof instead of knowing the lemmas example {α : Type _} (s : Set α) : Filter α := { sets := { t | s ⊆ t } univ_sets := subset_univ s sets_of_superset := fun hU hUV => Subset.trans hU hUV inter_sets := fun hU hV => subset_inter hU hV } example : Filter ℕ := { sets := { s | ∃ a, ∀ b, a ≤ b → b ∈ s } univ_sets := by use 42 simp sets_of_superset := by rintro U V ⟨N, hN⟩ hUV use N tauto inter_sets := by rintro U V ⟨N, hN⟩ ⟨N', hN'⟩ use max N N' intro b hb rw [max_le_iff] at hb constructor <;> tauto } def Tendsto₁ {X Y : Type _} (f : X → Y) (F : Filter X) (G : Filter Y) := ∀ V ∈ G, f ⁻¹' V ∈ F example {X Y Z : Type _} {F : Filter X} {G : Filter Y} {H : Filter Z} {f : X → Y} {g : Y → Z} (hf : Tendsto₁ f F G) (hg : Tendsto₁ g G H) : Tendsto₁ (g ∘ f) F H := calc map (g ∘ f) F = map g (map f F) := by rw [map_map] _ ≤ map g G := (map_mono hf) _ ≤ H := hg example {X Y Z : Type _} {F : Filter X} {G : Filter Y} {H : Filter Z} {f : X → Y} {g : Y → Z} (hf : Tendsto₁ f F G) (hg : Tendsto₁ g G H) : Tendsto₁ (g ∘ f) F H := by intro V hV rw [preimage_comp] apply hf apply hg exact hV example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) : Tendsto f atTop (𝓝 (x₀, y₀)) ↔ Tendsto (Prod.fst ∘ f) atTop (𝓝 x₀) ∧ Tendsto (Prod.snd ∘ f) atTop (𝓝 y₀) := calc Tendsto f atTop (𝓝 (x₀, y₀)) ↔ map f atTop ≤ 𝓝 (x₀, y₀) := Iff.rfl _ ↔ map f atTop ≤ 𝓝 x₀ ×ᶠ 𝓝 y₀ := by rw [nhds_prod_eq] _ ↔ map f atTop ≤ comap Prod.fst (𝓝 x₀) ⊓ comap Prod.snd (𝓝 y₀) := Iff.rfl _ ↔ map f atTop ≤ comap Prod.fst (𝓝 x₀) ∧ map f atTop ≤ comap Prod.snd (𝓝 y₀) := le_inf_iff _ ↔ map Prod.fst (map f atTop) ≤ 𝓝 x₀ ∧ map Prod.snd (map f atTop) ≤ 𝓝 y₀ := by rw [← map_le_iff_le_comap, ← map_le_iff_le_comap] _ ↔ map (Prod.fst ∘ f) atTop ≤ 𝓝 x₀ ∧ map (Prod.snd ∘ f) atTop ≤ 𝓝 y₀ := by rw [map_map, map_map] -- an alternative solution example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) : Tendsto f atTop (𝓝 (x₀, y₀)) ↔ Tendsto (Prod.fst ∘ f) atTop (𝓝 x₀) ∧ Tendsto (Prod.snd ∘ f) atTop (𝓝 y₀) := by rw [nhds_prod_eq] unfold Tendsto Filter.prod rw [le_inf_iff, ← map_le_iff_le_comap, map_map, ← map_le_iff_le_comap, map_map] example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x)) (huM : ∀ᶠ n in atTop, u n ∈ M) : x ∈ closure M := mem_closure_iff_clusterPt.mpr (neBot_of_le <| le_inf hux <| le_principal_iff.mpr huM)
-
-
-
@@ -1,365 +0,0 @@import Mathlib.Topology.Instances.Real import Mathlib.Analysis.NormedSpace.BanachSteinhaus open Set Filter open Topology Filter variable {X : Type _} [MetricSpace X] (a b c : X) #check (dist a b : ℝ) #check (dist_nonneg : 0 ≤ dist a b) #check (dist_eq_zero : dist a b = 0 ↔ a = b) #check (dist_comm a b : dist a b = dist b a) #check (dist_triangle a b c : dist a c ≤ dist a b + dist b c) -- Note the next three lines are not quoted, their purpose is to make sure those things don't get renamed while we're looking elsewhere. #check EMetricSpace #check PseudoMetricSpace #check PseudoEMetricSpace example {u : ℕ → X} {a : X} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := Metric.tendsto_atTop example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} : Continuous f ↔ ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := Metric.continuous_iff example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := by continuity example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := continuous_dist.comp ((hf.comp continuous_fst).prod_mk (hf.comp continuous_snd)) example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := by apply Continuous.dist exact hf.comp continuous_fst exact hf.comp continuous_snd example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := (hf.comp continuous_fst).dist (hf.comp continuous_snd) example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X => dist (f p.1) (f p.2) := hf.fst'.dist hf.snd' example {f : ℝ → X} (hf : Continuous f) : Continuous fun x : ℝ => f (x ^ 2 + x) := sorry example {f : ℝ → X} (hf : Continuous f) : Continuous fun x : ℝ => f (x ^ 2 + x) := hf.comp <| (continuous_pow 2).add continuous_id example {X Y : Type _} [MetricSpace X] [MetricSpace Y] (f : X → Y) (a : X) : ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x}, dist x a < δ → dist (f x) (f a) < ε := Metric.continuousAt_iff variable (r : ℝ) example : Metric.ball a r = { b | dist b a < r } := rfl example : Metric.closedBall a r = { b | dist b a ≤ r } := rfl example (hr : 0 < r) : a ∈ Metric.ball a r := Metric.mem_ball_self hr example (hr : 0 ≤ r) : a ∈ Metric.closedBall a r := Metric.mem_closedBall_self hr example (s : Set X) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s := Metric.isOpen_iff example {s : Set X} : IsClosed s ↔ IsOpen (sᶜ) := isOpen_compl_iff.symm example {s : Set X} (hs : IsClosed s) {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) (hus : ∀ n, u n ∈ s) : a ∈ s := hs.mem_of_tendsto hu (eventually_of_forall hus) example {s : Set X} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, a ∈ Metric.ball b ε := Metric.mem_closure_iff example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := sorry example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := by rw [Metric.tendsto_atTop] at hu rw [Metric.mem_closure_iff] intro ε ε_pos rcases hu ε ε_pos with ⟨N, hN⟩ refine' ⟨u N, hs _, _⟩ rw [dist_comm] exact hN N le_rfl example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s := Metric.nhds_basis_ball.mem_iff example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.closedBall x ε ⊆ s := Metric.nhds_basis_closedBall.mem_iff example : IsCompact (Set.Icc 0 1 : Set ℝ) := isCompact_Icc example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) := hs.tendsto_subseq hu example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f s) : ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y := hs.exists_forall_le hs' hfs example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f s) : ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x := hs.exists_forall_ge hs' hfs example {s : Set X} (hs : IsCompact s) : IsClosed s := hs.IsClosed example {X : Type _} [MetricSpace X] [CompactSpace X] : IsCompact (univ : Set X) := isCompact_univ #check IsCompact.isClosed example {X : Type _} [MetricSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := Metric.uniformContinuous_iff example {X : Type _} [MetricSpace X] [CompactSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} (hf : Continuous f) : UniformContinuous f := sorry example {X : Type _} [MetricSpace X] [CompactSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} (hf : Continuous f) : UniformContinuous f := by rw [Metric.uniformContinuous_iff] intro ε ε_pos let φ : X × X → ℝ := fun p => dist (f p.1) (f p.2) have φ_cont : Continuous φ := hf.fst'.dist hf.snd' let K := { p : X × X | ε ≤ φ p } have K_closed : IsClosed K := isClosed_le continuous_const φ_cont have K_cpct : IsCompact K := K_closed.is_compact cases' eq_empty_or_nonempty K with hK hK · use 1, by norm_num intro x y hxy have : (x, y) ∉ K := by simp [hK] simpa [K] · rcases K_cpct.exists_forall_le hK continuous_dist.continuous_on with ⟨⟨x₀, x₁⟩, xx_in, H⟩ use dist x₀ x₁ constructor · change _ < _ rw [dist_pos] intro h have : ε ≤ 0 := by simpa [*] using xx_in linarith · intro x x' contrapose! intro hxx' exact H (x, x') hxx' example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := Metric.cauchySeq_iff example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := Metric.cauchySeq_iff' example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete hu open BigOperators open Finset theorem cauchySeq_of_le_geometric_two' {u : ℕ → X} (hu : ∀ n : ℕ, dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : CauchySeq u := by rw [Metric.cauchySeq_iff'] intro ε ε_pos obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε := by sorry use N intro n hn obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn calc dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2) ^ i := sorry _ ≤ 1 / 2 ^ N * 2 := sorry _ < ε := sorry example {u : ℕ → X} (hu : ∀ n : ℕ, dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : CauchySeq u := by rw [Metric.cauchySeq_iff'] intro ε ε_pos obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε := by have : Tendsto (fun N : ℕ => (1 / 2 ^ N * 2 : ℝ)) atTop (𝓝 0) := by rw [← MulZeroClass.zero_mul (2 : ℝ)] apply Tendsto.mul simp_rw [← one_div_pow (2 : ℝ)] apply tendsto_pow_atTop_nhds_0_of_lt_1 <;> linarith exact tendsto_const_nhds rcases(atTop_basis.tendsto_iff (nhds_basis_Ioo_pos (0 : ℝ))).mp this ε ε_pos with ⟨N, H, hN⟩ exact ⟨N, by simpa using (hN N le_rfl).2⟩ use N intro n hn obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn calc dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := by rw [dist_comm, add_zero] _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := (dist_le_range_sum_dist (fun i => u (N + i)) k) _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := (sum_le_sum fun i hi => hu <| N + i) _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2) ^ i := by simp_rw [← one_div_pow, pow_add, ← mul_sum] _ ≤ 1 / 2 ^ N * 2 := (mul_le_mul_of_nonneg_left (sum_geometric_two_le _) (one_div_nonneg.mpr (pow_nonneg (zero_le_two : (0 : ℝ) ≤ 2) _))) _ < ε := hN open Metric example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : ∀ n, Dense (f n)) : Dense (⋂ n, f n) := by let B : ℕ → ℝ := fun n => (1 / 2) ^ n have Bpos : ∀ n, 0 < B n sorry /- Translate the density assumption into two functions `center` and `radius` associating to any n, x, δ, δpos a center and a positive radius such that `closed_ball center radius` is included both in `f n` and in `closed_ball x δ`. We can also require `radius ≤ (1/2)^(n+1)`, to ensure we get a Cauchy sequence later. -/ have : ∀ (n : ℕ) (x : X), ∀ δ > 0, ∃ y : X, ∃ r > 0, r ≤ B (n + 1) ∧ closed_ball y r ⊆ closed_ball x δ ∩ f n := by sorry choose! center radius Hpos HB Hball using this intro x rw [mem_closure_iff_nhds_basis nhds_basis_closed_ball] intro ε εpos /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball `closed_ball (c n) (r n)` is included in the previous ball and in `f n`, and such that `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs to all the `f n`. -/ let F : ℕ → X × ℝ := fun n => Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) let c : ℕ → X := fun n => (F n).1 let r : ℕ → ℝ := fun n => (F n).2 have rpos : ∀ n, 0 < r n := by sorry have rB : ∀ n, r n ≤ B n := by sorry have incl : ∀ n, closed_ball (c (n + 1)) (r (n + 1)) ⊆ closed_ball (c n) (r n) ∩ f n := by sorry have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by sorry have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`. rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩ -- this point `y` will be the desired point. We will check that it belongs to all -- `f n` and to `ball x ε`. use y have I : ∀ n, ∀ m ≥ n, closed_ball (c m) (r m) ⊆ closed_ball (c n) (r n) := by sorry have yball : ∀ n, y ∈ closed_ball (c n) (r n) := by sorry sorry example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : ∀ n, Dense (f n)) : Dense (⋂ n, f n) := by let B : ℕ → ℝ := fun n => (1 / 2) ^ n have Bpos : ∀ n, 0 < B n := fun n => pow_pos sorry n /- Translate the density assumption into two functions `center` and `radius` associating to any n, x, δ, δpos a center and a positive radius such that `closed_ball center radius` is included both in `f n` and in `closed_ball x δ`. We can also require `radius ≤ (1/2)^(n+1)`, to ensure we get a Cauchy sequence later. -/ have : ∀ (n : ℕ) (x : X), ∀ δ > 0, ∃ y : X, ∃ r > 0, r ≤ B (n + 1) ∧ closed_ball y r ⊆ closed_ball x δ ∩ f n := by intro n x δ δpos have : x ∈ closure (f n) := hd n x rcases Metric.mem_closure_iff.1 this (δ / 2) (half_pos δpos) with ⟨y, ys, xy⟩ rw [dist_comm] at xy obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closed_ball y r ⊆ f n := nhds_basis_closed_ball.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys) refine' ⟨y, min (min (δ / 2) r) (B (n + 1)), _, _, fun z hz => ⟨_, _⟩⟩ show 0 < min (min (δ / 2) r) (B (n + 1)) exact lt_min (lt_min (half_pos δpos) rpos) (Bpos (n + 1)) show min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1) exact min_le_right _ _ show z ∈ closed_ball x δ exact calc dist z x ≤ dist z y + dist y x := dist_triangle _ _ _ _ ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2 := (add_le_add hz xy.le) _ ≤ δ / 2 + δ / 2 := (add_le_add_right ((min_le_left _ _).trans (min_le_left _ _)) _) _ = δ := add_halves δ show z ∈ f n exact hr (calc dist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz _ ≤ r := (min_le_left _ _).trans (min_le_right _ _) ) choose! center radius Hpos HB Hball using this refine' fun x => (mem_closure_iff_nhds_basis nhds_basis_closed_ball).2 fun ε εpos => _ /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball `closed_ball (c n) (r n)` is included in the previous ball and in `f n`, and such that `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs to all the `f n`. -/ let F : ℕ → X × ℝ := fun n => Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) let c : ℕ → X := fun n => (F n).1 let r : ℕ → ℝ := fun n => (F n).2 have rpos : ∀ n, 0 < r n := by intro n induction' n with n hn exact lt_min εpos (Bpos 0) exact Hpos n (c n) (r n) hn have rB : ∀ n, r n ≤ B n := by intro n induction' n with n hn exact min_le_right _ _ exact HB n (c n) (r n) (rpos n) have incl : ∀ n, closed_ball (c (n + 1)) (r (n + 1)) ⊆ closed_ball (c n) (r n) ∩ f n := fun n => Hball n (c n) (r n) (rpos n) have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by intro n rw [dist_comm] have A : c (n + 1) ∈ closed_ball (c (n + 1)) (r (n + 1)) := mem_closed_ball_self (rpos <| n + 1).le have I := calc closed_ball (c (n + 1)) (r (n + 1)) ⊆ closed_ball (c n) (r n) := (incl n).trans (inter_subset_left _ _) _ ⊆ closed_ball (c n) (B n) := closed_ball_subset_closed_ball (rB n) exact I A have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`. rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩ -- this point `y` will be the desired point. We will check that it belongs to all -- `f n` and to `ball x ε`. use y have I : ∀ n, ∀ m ≥ n, closed_ball (c m) (r m) ⊆ closed_ball (c n) (r n) := by intro n refine' Nat.le_induction _ fun m hnm h => _ · exact Subset.rfl · exact (incl m).trans ((Set.inter_subset_left _ _).trans h) have yball : ∀ n, y ∈ closed_ball (c n) (r n) := by intro n refine' is_closed_ball.mem_of_tendsto ylim _ refine' (Filter.eventually_ge_atTop n).mono fun m hm => _ exact I n m hm (mem_closed_ball_self (rpos _).le) constructor · suffices ∀ n, y ∈ f n by rwa [Set.mem_iInter] intro n have : closed_ball (c (n + 1)) (r (n + 1)) ⊆ f n := Subset.trans (incl n) (inter_subset_right _ _) exact this (yball (n + 1)) calc dist y x ≤ r 0 := yball 0 _ ≤ ε := min_le_left _ _
-
-
-
@@ -1,202 +0,0 @@import Mathlib.Topology.Instances.Real import Mathlib.Analysis.NormedSpace.BanachSteinhaus open Set Filter open Topology Filter section variable {X : Type _} [TopologicalSpace X] example : IsOpen (univ : Set X) := isOpen_univ example : IsOpen (∅ : Set X) := isOpen_empty example {ι : Type _} {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋃ i, s i) := isOpen_iUnion hs example {ι : Type _} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋂ i, s i) := isOpen_iInter hs variable {Y : Type _} [TopologicalSpace Y] example {f : X → Y} : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) := continuous_def example {f : X → Y} {x : X} : ContinuousAt f x ↔ map f (𝓝 x) ≤ 𝓝 (f x) := Iff.rfl example {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ U ∈ 𝓝 (f x), ∀ᶠ x in 𝓝 x, f x ∈ U := Iff.rfl example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := mem_nhds_iff example (x : X) : pure x ≤ 𝓝 x := pure_le_nhds x example (x : X) (P : X → Prop) (h : ∀ᶠ y in 𝓝 x, P y) : P x := pure_le_nhds x h example {P : X → Prop} {x : X} (h : ∀ᶠ y in 𝓝 x, P y) : ∀ᶠ y in 𝓝 x, ∀ᶠ z in 𝓝 y, P z := eventually_eventually_nhds.mpr h #check TopologicalSpace.mkOfNhds #check TopologicalSpace.nhds_mkOfNhds example {α : Type _} (n : α → Filter α) (H₀ : ∀ a, pure a ≤ n a) (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x) : ∀ a, ∀ s ∈ n a, ∃ t ∈ n a, t ⊆ s ∧ ∀ a' ∈ t, s ∈ n a' := sorry example {α : Type _} (n : α → Filter α) (H₀ : ∀ a, pure a ≤ n a) (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x) : ∀ a, ∀ s ∈ n a, ∃ t ∈ n a, t ⊆ s ∧ ∀ a' ∈ t, s ∈ n a' := by intro a s s_in refine' ⟨{ y | s ∈ n y }, H a (fun x => x ∈ s) s_in, _, by tauto⟩ rintro y (hy : s ∈ n y) exact H₀ y hy end -- BOTH. variable {X Y : Type _} example (f : X → Y) : TopologicalSpace X → TopologicalSpace Y := TopologicalSpace.coinduced f example (f : X → Y) : TopologicalSpace Y → TopologicalSpace X := TopologicalSpace.induced f example (f : X → Y) (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) : TopologicalSpace.coinduced f T_X ≤ T_Y ↔ T_X ≤ TopologicalSpace.induced f T_Y := coinduced_le_iff_le_induced #check coinduced_compose #check induced_compose example {T T' : TopologicalSpace X} : T ≤ T' ↔ ∀ s, T'.IsOpen s → T.IsOpen s := Iff.rfl example (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) (f : X → Y) : Continuous f ↔ TopologicalSpace.coinduced f T_X ≤ T_Y := continuous_iff_coinduced_le example {Z : Type _} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z) (g : Y → Z) : @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔ @Continuous X Z T_X T_Z (g ∘ f) := by rw [continuous_iff_coinduced_le, coinduced_compose, continuous_iff_coinduced_le] example (ι : Type _) (X : ι → Type _) (T_X : ∀ i, TopologicalSpace <| X i) : (Pi.topologicalSpace : TopologicalSpace (∀ i, X i)) = ⨅ i, TopologicalSpace.induced (fun x => x i) (T_X i) := rfl example [TopologicalSpace X] [T2Space X] {u : ℕ → X} {a b : X} (ha : Tendsto u atTop (𝓝 a)) (hb : Tendsto u atTop (𝓝 b)) : a = b := tendsto_nhds_unique ha hb example [TopologicalSpace X] [RegularSpace X] (a : X) : (𝓝 a).HasBasis (fun s : Set X => s ∈ 𝓝 a ∧ IsClosed s) id := closed_nhds_basis a example [TopologicalSpace X] {x : X} : (𝓝 x).HasBasis (fun t : Set X => t ∈ 𝓝 x ∧ IsOpen t) id := nhds_basis_opens' x theorem aux {X Y A : Type _} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := sorry example {X Y A : Type _} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := by simpa [and_assoc] using ((nhds_basis_opens' x).comap c).tendsto_left_iff.mp h V' V'_in example [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] {A : Set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f) (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) <| 𝓝 x) <| 𝓝 c) : ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := sorry #check @HasBasis.tendsto_right_iff example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f) (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) <| 𝓝 x) <| 𝓝 c) : ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := by choose φ hφ using hf use φ constructor · rw [continuous_iff_continuousAt] intro x suffices ∀ V' ∈ 𝓝 (φ x), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 x by simp [ContinuousAt, (closed_nhds_basis _).tendsto_right_iff] intro V' V'_in V'_closed obtain ⟨V, V_in, V_op, hV⟩ : ∃ V ∈ 𝓝 x, IsOpen V ∧ (↑) ⁻¹' V ⊆ f ⁻¹' V' := aux (hφ x) V'_in suffices : ∀ y ∈ V, φ y ∈ V' exact mem_of_superset V_in this intro y y_in have hVx : V ∈ 𝓝 y := V_op.mem_nhds y_in haveI : (comap ((↑) : A → X) (𝓝 y)).NeBot := by simpa [mem_closure_iff_comap_neBot] using hA y apply V'_closed.mem_of_tendsto (hφ y) exact mem_of_superset (preimage_mem_comap hVx) hV · intro a have lim : Tendsto f (𝓝 a) (𝓝 <| φ a) := by simpa [nhds_induced] using hφ a exact tendsto_nhds_unique limUnder f_cont.continuousAt example [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] {s : Set X} {a : X} : a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) := mem_closure_iff_seq_limit variable [TopologicalSpace X] example {F : Filter X} {x : X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) := Iff.rfl example {s : Set X} : IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := Iff.rfl example [TopologicalSpace.FirstCountableTopology X] {s : Set X} {u : ℕ → X} (hs : IsCompact s) (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) := hs.tendsto_subseq hu variable [TopologicalSpace Y] example {x : X} {F : Filter X} {G : Filter Y} (H : ClusterPt x F) {f : X → Y} (hfx : ContinuousAt f x) (hf : Tendsto f F G) : ClusterPt (f x) G := ClusterPt.map H hfx hf example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) : IsCompact (f '' s) := by intro F F_ne F_le have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F := by sorry have Hne : (𝓟 s ⊓ comap f F).NeBot := by sorry have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s := inf_le_left sorry example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) : IsCompact (f '' s) := by intro F F_ne F_le have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F := by rw [Filter.push_pull, map_principal] have Hne : (𝓟 s ⊓ comap f F).NeBot := by apply NeBot.of_map rwa [map_eq, inf_of_le_right F_le] have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s := inf_le_left rcases hs Hle with ⟨x, x_in, hx⟩ refine' ⟨f x, mem_image_of_mem f x_in, _⟩ apply hx.map hf.continuousAt rw [Tendsto, map_eq] exact inf_le_right example {ι : Type _} {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i := hs.elim_finite_subcover U hUo hsU example [CompactSpace X] : IsCompact (univ : Set X) := isCompact_univ
-
-