Changes
61 changed files (+0/-7837)
-
-
-
@@ -1,1 +0,0 @@#eval "Hello, World!"
-
-
src/01_Introduction/02_Overview.lean (deleted)
-
@@ -1,62 +0,0 @@import data.nat.basic import data.nat.parity import tactic open nat /- These are pieces of data. -/ #check 2 + 2 def f (x : ℕ) := x + 3 #check f /- These are propositions, of type `Prop`. -/ #check 2 + 2 = 4 def fermat_last_theorem := ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x^n + y^n ≠ z^n #check fermat_last_theorem /- These are proofs of propositions. -/ theorem easy : 2 + 2 = 4 := rfl #check easy theorem hard : fermat_last_theorem := sorry #check hard /- Here are some proofs. -/ example : ∀ m n : nat, even n → even (m * n) := assume m n ⟨k, (hk : n = k + k)⟩, have hmn : m * n = m * k + m * k, by rw [hk, mul_add], show ∃ l, m * n = l + l, from ⟨_, hmn⟩ example : ∀ m n : nat, even n → even (m * n) := λ m n ⟨k, hk⟩, ⟨m * k, by rw [hk, mul_add]⟩ example : ∀ m n : nat, even n → even (m * n) := begin -- say m and n are natural numbers, and assume n=2*k rintros m n ⟨k, hk⟩, -- We need to prove m*n is twice a natural. Let's show it's twice m*k. use m * k, -- substitute in for n rw hk, -- and now it's obvious ring end example : ∀ m n : nat, even n → even (m * n) := by { rintros m n ⟨k, hk⟩, use m * k, rw hk, ring } example : ∀ m n : nat, even n → even (m * n) := by intros; simp * with parity_simps
-
-
-
-
@@ -1,6 +0,0 @@import data.nat.basic import data.nat.parity import tactic open nat -- There are no exercises in this section.
-
-
src/02_Basics/01_Calculating.lean (deleted)
-
@@ -1,192 +0,0 @@import data.real.basic /- An example. -/ import data.real.basic example (a b c : ℝ) : (a * b) * c = b * (a * c) := begin rw mul_comm a b, rw mul_assoc b a c end /- Try these.-/ example (a b c : ℝ) : (c * b) * a = b * (a * c) := begin sorry end example (a b c : ℝ) : a * (b * c) = b * (a * c) := begin sorry end /- An example. -/ example (a b c : ℝ) : a * b * c = b * c * a := begin rw mul_assoc, rw mul_comm end /- Try doing the first of these without providing any arguments at all, and the second with only one argument. -/ example (a b c : ℝ) : a * (b * c) = b * (c * a) := begin sorry end example (a b c : ℝ) : a * (b * c) = b * (a * c) := begin sorry end /- Using facts from the local context. -/ example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := begin rw h', rw ←mul_assoc, rw h, rw mul_assoc end /- Try these. For the second one, use the theorem `sub_self`. -/ example (a b c d e f : ℝ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := begin sorry end example (a b c d : ℝ) (hyp : c = b * a - d) (hyp' : d = a * b) : c = 0 := begin sorry end /- Examples. -/ example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by rw [h', ←mul_assoc, h, mul_assoc] section variables a b c d e f g : ℝ example (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by rw [h', ←mul_assoc, h, mul_assoc] end section variables a b c : ℝ #check a #check a + b #check (a : ℝ) #check mul_comm a b #check (mul_comm a b : a * b = b * a) #check mul_assoc c a b #check mul_comm a #check mul_comm #check @mul_comm end section variables a b : ℝ example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := begin rw [mul_add, add_mul, add_mul], rw [←add_assoc, add_assoc (a * a)], rw [mul_comm b a, ←two_mul] end example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := calc (a + b) * (a + b) = a * a + b * a + (a * b + b * b) : by rw [mul_add, add_mul, add_mul] ... = a * a + (b * a + a * b) + b * b : by rw [←add_assoc, add_assoc (a * a)] ... = a * a + 2 * (a * b) + b * b : by rw [mul_comm b a, ←two_mul] example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := calc (a + b) * (a + b) = a * a + b * a + (a * b + b * b) : begin sorry end ... = a * a + (b * a + a * b) + b * b : by sorry ... = a * a + 2 * (a * b) + b * b : by sorry end /- Try these. For the second, use the theorems listed underneath. -/ section variables a b c d : ℝ example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := sorry example (a b : ℝ) : (a + b) * (a - b) = a^2 - b^2 := begin sorry end #check pow_two a #check mul_sub a b c #check add_mul a b c #check add_sub a b c #check sub_sub a b c #check add_zero a end /- Examples. -/ section variables a b c d : ℝ example (a b c d : ℝ) (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := begin rw hyp' at hyp, rw mul_comm d a at hyp, rw ← two_mul (a * d) at hyp, rw ← mul_assoc 2 a d at hyp, exact hyp end example : (c * b) * a = b * (a * c) := by ring example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring example : (a + b) * (a - b) = a^2 - b^2 := by ring example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := begin rw [hyp, hyp'], ring end end example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := begin nth_rewrite 1 h, rw add_mul end
-
-
-
@@ -1,157 +0,0 @@import algebra.ring import data.real.basic import tactic section variables (R : Type*) [ring R] #check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c)) #check (add_comm : ∀ a b : R, a + b = b + a) #check (zero_add : ∀ a : R, 0 + a = a) #check (add_left_neg : ∀ a : R, -a + a = 0) #check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c)) #check (mul_one : ∀ a : R, a * 1 = a) #check (one_mul : ∀ a : R, 1 * a = a) #check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c) #check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c) end section variables (R : Type*) [comm_ring R] variables a b c d : R example : (c * b) * a = b * (a * c) := by ring example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring example : (a + b) * (a - b) = a^2 - b^2 := by ring example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := begin rw [hyp, hyp'], ring end end namespace my_ring variables {R : Type*} [ring R] theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add] theorem add_right_neg (a : R) : a + -a = 0 := by rw [add_comm, add_left_neg] #check @my_ring.add_zero #check @add_zero end my_ring namespace my_ring variables {R : Type*} [ring R] theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b := by rw [←add_assoc, add_left_neg, zero_add] /- Prove these: -/ theorem add_neg_cancel_right (a b : R) : (a + b) + -b = a := sorry theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := sorry theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := sorry theorem mul_zero (a : R) : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, { rw [←mul_add, add_zero, add_zero] }, rw add_left_cancel h end theorem zero_mul (a : R) : 0 * a = 0 := sorry theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := sorry theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := sorry theorem neg_zero : (-0 : R) = 0 := begin apply neg_eq_of_add_eq_zero, rw add_zero end theorem neg_neg (a : R) : -(-a) = a := sorry end my_ring /- Examples. -/ section variables {R : Type*} [ring R] example (a b : R) : a - b = a + -b := sub_eq_add_neg a b end example (a b : ℝ) : a - b = a + -b := rfl example (a b : ℝ) : a - b = a + -b := by reflexivity namespace my_ring variables {R : Type*} [ring R] theorem self_sub (a : R) : a - a = 0 := sorry lemma one_add_one_eq_two : 1 + 1 = (2 : R) := by refl theorem two_mul (a : R) : 2 * a = a + a := sorry end my_ring section variables (A : Type*) [add_group A] #check (add_assoc : ∀ a b c : A, a + b + c = a + (b + c)) #check (zero_add : ∀ a : A, 0 + a = a) #check (add_left_neg : ∀ a : A, -a + a = 0) end section variables {G : Type*} [group G] #check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)) #check (one_mul : ∀ a : G, 1 * a = a) #check (mul_left_inv : ∀ a : G, a⁻¹ * a = 1) namespace my_group theorem mul_right_inv (a : G) : a * a⁻¹ = 1 := sorry theorem mul_one (a : G) : a * 1 = a := sorry theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a ⁻¹ := sorry end my_group end
-
-
-
@@ -1,159 +0,0 @@import analysis.special_functions.log.basic variables a b c d e : ℝ open real #check (le_refl : ∀ a : ℝ, a ≤ a) #check (le_trans : a ≤ b → b ≤ c → a ≤ c) section variables (h : a ≤ b) (h' : b ≤ c) #check (le_refl : ∀ a : real, a ≤ a) #check (le_refl a : a ≤ a) #check (le_trans : a ≤ b → b ≤ c → a ≤ c) #check (le_trans h : b ≤ c → a ≤ c) #check (le_trans h h' : a ≤ c) end example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := begin apply le_trans, { apply h₀ }, apply h₁ end example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := begin apply le_trans h₀, apply h₁ end example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by exact le_trans h₀ h₁ example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := le_trans h₀ h₁ example (x : ℝ) : x ≤ x := by apply le_refl example (x : ℝ) : x ≤ x := by exact le_refl x example (x : ℝ) : x ≤ x := le_refl x #check (le_refl : ∀ a, a ≤ a) #check (le_trans : a ≤ b → b ≤ c → a ≤ c) #check (lt_of_le_of_lt : a ≤ b → b < c → a < c) #check (lt_of_lt_of_le : a < b → b ≤ c → a < c) #check (lt_trans : a < b → b < c → a < c) /- Try this. -/ example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := sorry example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by linarith section example (h : 2 * a ≤ 3 * b) (h' : 1 ≤ a) (h'' : d = 2) : d + a ≤ 5 * b := by linarith end example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by linarith [exp_le_exp.mpr h'] #check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b) #check (exp_lt_exp : exp a < exp b ↔ a < b) #check (log_le_log : 0 < a → 0 < b → (log a ≤ log b ↔ a ≤ b)) #check (log_lt_log : 0 < a → a < b → log a < log b) #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d) #check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b) #check (add_le_add_right : a ≤ b → ∀ c, a + c ≤ b + c) #check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d) #check (add_lt_add_of_lt_of_le : a < b → c ≤ d → a + c < b + d) #check (add_lt_add_left : a < b → ∀ c, c + a < c + b) #check (add_lt_add_right : a < b → ∀ c, a + c < b + c) #check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b) #check (add_pos : 0 < a → 0 < b → 0 < a + b) #check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b) #check (exp_pos : ∀ a, 0 < exp a) #check @add_le_add_left example (h : a ≤ b) : exp a ≤ exp b := begin rw exp_le_exp, exact h end example (h₀ : a ≤ b) (h₁ : c < d) : a + exp c + e < b + exp d + e := begin apply add_lt_add_of_lt_of_le, { apply add_lt_add_of_le_of_lt h₀, apply exp_lt_exp.mpr h₁ }, apply le_refl end example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := begin sorry end example : (0 : ℝ) < 1 := by norm_num example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := begin have h₀ : 0 < 1 + exp a, { sorry }, have h₁ : 0 < 1 + exp b, { sorry }, apply (log_le_log h₀ h₁).mpr, sorry end example : 0 ≤ a^2 := begin -- library_search, exact pow_two_nonneg a end example (h : a ≤ b) : c - exp b ≤ c - exp a := sorry example : 2*a*b ≤ a^2 + b^2 := begin have h : 0 ≤ a^2 - 2*a*b + b^2, calc a^2 - 2*a*b + b^2 = (a - b)^2 : by ring ... ≥ 0 : by apply pow_two_nonneg, calc 2*a*b = 2*a*b + 0 : by ring ... ≤ 2*a*b + (a^2 - 2*a*b + b^2) : add_le_add (le_refl _) h ... = a^2 + b^2 : by ring end example : 2*a*b ≤ a^2 + b^2 := begin have h : 0 ≤ a^2 - 2*a*b + b^2, calc a^2 - 2*a*b + b^2 = (a - b)^2 : by ring ... ≥ 0 : by apply pow_two_nonneg, linarith end example : abs (a*b) ≤ (a^2 + b^2) / 2 := sorry #check abs_le'.mpr
-
-
-
@@ -1,93 +0,0 @@import data.real.basic section variables a b c d : ℝ #check (min_le_left a b : min a b ≤ a) #check (min_le_right a b : min a b ≤ b) #check (le_min : c ≤ a → c ≤ b → c ≤ min a b) example : min a b = min b a := begin apply le_antisymm, { show min a b ≤ min b a, apply le_min, { apply min_le_right }, apply min_le_left }, { show min b a ≤ min a b, apply le_min, { apply min_le_right }, apply min_le_left } end example : min a b = min b a := begin have h : ∀ x y, min x y ≤ min y x, { intros x y, apply le_min, apply min_le_right, apply min_le_left }, apply le_antisymm, apply h, apply h end example : min a b = min b a := begin apply le_antisymm, repeat { apply le_min, apply min_le_right, apply min_le_left } end example : max a b = max b a := sorry example : min (min a b) c = min a (min b c) := sorry lemma aux : min a b + c ≤ min (a + c) (b + c) := sorry example : min a b + c = min (a + c) (b + c) := sorry #check (abs_add : ∀ a b : ℝ, abs (a + b) ≤ abs a + abs b) example : abs a - abs b ≤ abs (a - b) := sorry end section variables w x y z : ℕ example (h₀ : x ∣ y) (h₁ : y ∣ z) : x ∣ z := dvd_trans h₀ h₁ example : x ∣ y * x * z := begin apply dvd_mul_of_dvd_left, apply dvd_mul_left end example : x ∣ x^2 := by apply dvd_mul_right example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := sorry end section variables m n : ℕ open nat #check (gcd_zero_right n : gcd n 0 = n) #check (gcd_zero_left n : gcd 0 n = n) #check (lcm_zero_right n : lcm n 0 = 0) #check (lcm_zero_left n : lcm 0 n = 0) example : gcd m n = gcd n m := sorry end
-
-
-
@@ -1,99 +0,0 @@import topology.metric_space.basic section variables {α : Type*} [partial_order α] variables x y z : α #check x ≤ y #check (le_refl x : x ≤ x) #check (le_trans : x ≤ y → y ≤ z → x ≤ z) #check x < y #check (lt_irrefl x : ¬ x < x) #check (lt_trans : x < y → y < z → x < z) #check (lt_of_le_of_lt : x ≤ y → y < z → x < z) #check (lt_of_lt_of_le : x < y → y ≤ z → x < z) example : x < y ↔ x ≤ y ∧ x ≠ y := lt_iff_le_and_ne end section variables {α : Type*} [lattice α] variables x y z : α #check x ⊓ y #check (inf_le_left : x ⊓ y ≤ x) #check (inf_le_right : x ⊓ y ≤ y) #check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y) #check x ⊔ y #check (le_sup_left : x ≤ x ⊔ y) #check (le_sup_right: y ≤ x ⊔ y) #check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z) example : x ⊓ y = y ⊓ x := sorry example : x ⊓ y ⊓ z = x ⊓ (y ⊓ z) := sorry example : x ⊔ y = y ⊔ x := sorry example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := sorry theorem absorb1 : x ⊓ (x ⊔ y) = x := sorry theorem absorb2 : x ⊔ (x ⊓ y) = x := sorry end section variables {α : Type*} [distrib_lattice α] variables x y z : α #check (inf_sup_left : x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) #check (inf_sup_right : (x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)) #check (sup_inf_left : x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) #check (sup_inf_right : (x ⊓ y) ⊔ z = (x ⊔ z) ⊓ (y ⊔ z)) end section variables {α : Type*} [lattice α] variables a b c : α example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) := sorry example (h : ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c) := sorry end section variables {R : Type*} [ordered_ring R] variables a b c : R #check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b) #check (mul_pos : 0 < a → 0 < b → 0 < a * b) #check (mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b) example : a ≤ b → 0 ≤ b - a := sorry example : 0 ≤ b - a → a ≤ b := sorry example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := sorry end section variables {X : Type*} [metric_space X] variables x y z : X #check (dist_self x : dist x x = 0) #check (dist_comm x y : dist x y = dist y x) #check (dist_triangle x y z : dist x z ≤ dist x y + dist y z) example (x y : X) : 0 ≤ dist x y := sorry end
-
-
-
@@ -1,45 +0,0 @@import data.real.basic example (a b c : ℝ) : (c * b) * a = b * (a * c) := begin rw mul_comm c b, rw mul_assoc b c a, rw mul_comm c a end example (a b c : ℝ) : a * (b * c) = b * (a * c) := begin rw ←mul_assoc a b c, rw mul_comm a b, rw mul_assoc b a c end example (a b c : ℝ) : a * (b * c) = b * (c * a) := begin rw mul_comm, rw mul_assoc end example (a b c : ℝ) : a * (b * c) = b * (a * c) := begin rw ←mul_assoc, rw mul_comm a, rw mul_assoc end example (a b c d e f : ℝ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := begin rw mul_assoc a, rw h, rw ←mul_assoc end example (a b c d : ℝ) (hyp : c = b * a - d) (hyp' : d = a * b) : c = 0 := begin rw hyp, rw hyp', rw mul_comm, rw sub_self end
-
-
-
@@ -1,84 +0,0 @@import algebra.ring import data.real.basic import tactic namespace my_ring variables {R : Type*} [ring R] theorem add_neg_cancel_right (a b : R) : (a + b) + -b = a := by rw [add_assoc, add_right_neg, add_zero] theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by rw [←neg_add_cancel_left a b, h, neg_add_cancel_left] theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by rw [←add_neg_cancel_right a b, h, add_neg_cancel_right] theorem zero_mul (a : R) : 0 * a = 0 := begin have h : 0 * a + 0 * a = 0 * a + 0, { rw [←add_mul, add_zero, add_zero] }, rw add_left_cancel h end theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by rw [←neg_add_cancel_left a b, h, add_zero] theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := begin symmetry, apply neg_eq_of_add_eq_zero, rw [add_comm, h] end theorem neg_zero : (-0 : R) = 0 := begin apply neg_eq_of_add_eq_zero, rw add_zero end theorem neg_neg (a : R) : -(-a) = a := begin apply neg_eq_of_add_eq_zero, rw add_left_neg end end my_ring namespace my_ring variables {R : Type*} [ring R] theorem self_sub (a : R) : a - a = 0 := by rw [sub_eq_add_neg, add_right_neg] lemma one_add_one_eq_two : 1 + 1 = (2 : R) := by refl theorem two_mul (a : R) : 2 * a = a + a := by rw [←one_add_one_eq_two, add_mul, one_mul] end my_ring section variables {G : Type*} [group G] namespace my_group theorem mul_right_inv (a : G) : a * a⁻¹ = 1 := begin have h : (a * a⁻¹)⁻¹ * ((a * a⁻¹) * (a * a⁻¹)) = 1, { rw [mul_assoc, ←mul_assoc a⁻¹ a, mul_left_inv, one_mul, mul_left_inv] }, rw [←h, ←mul_assoc, mul_left_inv, one_mul] end theorem mul_one (a : G) : a * 1 = a := by rw [←mul_left_inv a, ←mul_assoc, mul_right_inv, one_mul] theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a ⁻¹ := by rw [←one_mul (b⁻¹ * a⁻¹), ←mul_left_inv (a * b), mul_assoc, mul_assoc, ←mul_assoc b b⁻¹, mul_right_inv, one_mul, mul_right_inv, mul_one] end my_group end
-
-
-
@@ -1,79 +0,0 @@import analysis.special_functions.log.basic variables a b c d e : ℝ open real example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := begin apply lt_of_le_of_lt h₀, apply lt_trans h₁, exact lt_of_le_of_lt h₂ h₃ end example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := begin apply add_le_add_left, rw exp_le_exp, apply add_le_add_left h₀ end -- an alterantive using `linarith`. example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := begin have : exp (a + d) ≤ exp (a + e), { rw exp_le_exp, linarith }, linarith [this] end example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := begin have h₀ : 0 < 1 + exp a, { linarith [exp_pos a]}, have h₁ : 0 < 1 + exp b, { linarith [exp_pos b] }, apply (log_le_log h₀ h₁).mpr, apply add_le_add_left (exp_le_exp.mpr h), end -- SOLUTION. example (h : a ≤ b) : c - exp b ≤ c - exp a := begin apply sub_le_sub_left, exact exp_le_exp.mpr h end -- alternatively: example (h : a ≤ b) : c - exp b ≤ c - exp a := by linarith [exp_le_exp.mpr h] theorem fact1 : a*b*2 ≤ a^2 + b^2 := begin have h : 0 ≤ a^2 - 2*a*b + b^2, calc a^2 - 2*a*b + b^2 = (a - b)^2 : by ring ... ≥ 0 : by apply pow_two_nonneg, linarith end theorem fact2 : -(a*b)*2 ≤ a^2 + b^2 := begin have h : 0 ≤ a^2 + 2*a*b + b^2, calc a^2 + 2*a*b + b^2 = (a + b)^2 : by ring ... ≥ 0 : by apply pow_two_nonneg, linarith end example : abs (a*b) ≤ (a^2 + b^2) / 2 := begin have h : (0 : ℝ) < 2, { norm_num }, apply abs_le'.mpr, split, { rw le_div_iff h, apply fact1 }, rw le_div_iff h, apply fact2, end
-
-
-
@@ -1,134 +0,0 @@import data.real.basic section variables a b c d : ℝ #check (min_le_left a b : min a b ≤ a) #check (min_le_right a b : min a b ≤ b) #check (le_min : c ≤ a → c ≤ b → c ≤ min a b) example : max a b = max b a := begin apply le_antisymm, repeat { apply max_le, apply le_max_right, apply le_max_left } end example : min (min a b) c = min a (min b c) := begin apply le_antisymm, { apply le_min, { apply le_trans, apply min_le_left, apply min_le_left }, apply le_min, { apply le_trans, apply min_le_left, apply min_le_right }, apply min_le_right }, apply le_min, { apply le_min, { apply min_le_left }, apply le_trans, apply min_le_right, apply min_le_left }, apply le_trans, apply min_le_right, apply min_le_right end lemma aux : min a b + c ≤ min (a + c) (b + c) := begin apply le_min, { apply add_le_add_right, apply min_le_left }, apply add_le_add_right, apply min_le_right end example : min a b + c = min (a + c) (b + c) := begin apply le_antisymm, { apply aux }, have h : min (a + c) (b + c) = min (a + c) (b + c) - c + c, { rw sub_add_cancel }, rw h, apply add_le_add_right, rw sub_eq_add_neg, apply le_trans, apply aux, rw [add_neg_cancel_right, add_neg_cancel_right] end example : abs a - abs b ≤ abs (a - b) := calc abs a - abs b = abs (a - b + b) - abs b : by rw sub_add_cancel ... ≤ abs (a - b) + abs b - abs b : begin apply sub_le_sub_right, apply abs_add end ... ≤ abs (a - b) : by rw add_sub_cancel -- alternatively example : abs a - abs b ≤ abs (a - b) := begin have h := abs_add (a - b) b, rw sub_add_cancel at h, linarith end end section variables w x y z : ℕ example (h₀ : x ∣ y) (h₁ : y ∣ z) : x ∣ z := dvd_trans h₀ h₁ example : x ∣ y * x * z := begin apply dvd_mul_of_dvd_left, apply dvd_mul_left end example : x ∣ x^2 := by apply dvd_mul_right example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := begin apply dvd_add, { apply dvd_add, { apply dvd_mul_of_dvd_right, apply dvd_mul_right }, apply dvd_mul_right }, rw pow_two, apply dvd_mul_of_dvd_right, exact h end end section variables m n : ℕ open nat #check (gcd_zero_right n : gcd n 0 = n) #check (gcd_zero_left n : gcd 0 n = n) #check (lcm_zero_right n : lcm n 0 = 0) #check (lcm_zero_left n : lcm 0 n = 0) example : gcd m n = gcd n m := begin apply dvd_antisymm, repeat { apply dvd_gcd, apply gcd_dvd_right, apply gcd_dvd_left } end end
-
-
-
@@ -1,159 +0,0 @@import topology.metric_space.basic section variables {α : Type*} [lattice α] variables x y z : α example : x ⊓ y = y ⊓ x := begin apply le_antisymm, repeat { apply le_inf, { apply inf_le_right }, apply inf_le_left } end example : x ⊓ y ⊓ z = x ⊓ (y ⊓ z) := begin apply le_antisymm, { apply le_inf, { apply le_trans, apply inf_le_left, apply inf_le_left }, apply le_inf, { apply le_trans, apply inf_le_left, apply inf_le_right }, apply inf_le_right }, apply le_inf, { apply le_inf, { apply inf_le_left }, apply le_trans, apply inf_le_right, apply inf_le_left }, apply le_trans, apply inf_le_right, apply inf_le_right end example : x ⊔ y = y ⊔ x := begin apply le_antisymm, repeat { apply sup_le, { apply le_sup_right }, apply le_sup_left } end example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := begin apply le_antisymm, { apply sup_le, { apply sup_le, apply le_sup_left, { apply le_trans, apply @le_sup_left _ _ y z, apply le_sup_right } }, apply le_trans, apply @le_sup_right _ _ y z, apply le_sup_right }, apply sup_le, { apply le_trans, apply @le_sup_left _ _ x y, apply le_sup_left }, apply sup_le, { apply le_trans, apply @le_sup_right _ _ x y, apply le_sup_left }, apply le_sup_right end theorem absorb1 : x ⊓ (x ⊔ y) = x := begin apply le_antisymm, { apply inf_le_left }, apply le_inf, { apply le_refl }, apply le_sup_left end theorem absorb2 : x ⊔ (x ⊓ y) = x := begin apply le_antisymm, { apply sup_le, { apply le_refl }, apply inf_le_left }, apply le_sup_left end end section variables {α : Type*} [distrib_lattice α] variables x y z : α #check (inf_sup_left : x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) #check (inf_sup_right : (x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)) #check (sup_inf_left : x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) #check (sup_inf_right : (x ⊓ y) ⊔ z = (x ⊔ z) ⊓ (y ⊔ z)) end section variables {α : Type*} [lattice α] variables a b c : α example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) := by rw [h, @inf_comm _ _ (a ⊔ b), absorb1, @inf_comm _ _ (a ⊔ b), h, ←sup_assoc, @inf_comm _ _ c a, absorb2, inf_comm] example (h : ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c) := by rw [h, @sup_comm _ _ (a ⊓ b), absorb2, @sup_comm _ _ (a ⊓ b), h, ←inf_assoc, @sup_comm _ _ c a, absorb1, sup_comm] end section variables {R : Type*} [ordered_ring R] variables a b c : R theorem aux1 : a ≤ b → 0 ≤ b - a := begin intro h, rw [←sub_self a, sub_eq_add_neg, sub_eq_add_neg, add_comm, add_comm b], apply add_le_add_left h end theorem aux2 : 0 ≤ b - a → a ≤ b := begin intro h, rw [←add_zero a, ←sub_add_cancel b a, add_comm (b - a)], apply add_le_add_left h end example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := begin have h1 : 0 ≤ (b - a) * c, { exact mul_nonneg (aux1 _ _ h) h' }, rw sub_mul at h1, exact aux2 _ _ h1 end end section variables {X : Type*} [metric_space X] variables x y z : X example (x y : X) : 0 ≤ dist x y := begin have : 0 ≤ dist x y + dist y x, { rw [←dist_self x], apply dist_triangle }, linarith [dist_comm x y] end end
-
-
-
@@ -1,188 +0,0 @@import data.real.basic #check ∀ x : ℝ, 0 ≤ x → abs x = x #check ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε lemma my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := sorry section variables a b δ : ℝ variables (h₀ : 0 < δ) (h₁ : δ ≤ 1) variables (ha : abs a < δ) (hb : abs b < δ) #check my_lemma a b δ #check my_lemma a b δ h₀ h₁ #check my_lemma a b δ h₀ h₁ ha hb end lemma my_lemma2 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := sorry section variables a b δ : ℝ variables (h₀ : 0 < δ) (h₁ : δ ≤ 1) variables (ha : abs a < δ) (hb : abs b < δ) #check my_lemma2 h₀ h₁ ha hb end lemma my_lemma3 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := begin intros x y ε epos ele1 xlt ylt, sorry end lemma my_lemma4 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := begin intros x y ε epos ele1 xlt ylt, calc abs (x * y) = abs x * abs y : sorry ... ≤ abs x * ε : sorry ... < 1 * ε : sorry ... = ε : sorry end def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x section variables (f g : ℝ → ℝ) (a b : ℝ) example (hfa : fn_ub f a) (hgb : fn_ub g b) : fn_ub (λ x, f x + g x) (a + b) := begin intro x, dsimp, apply add_le_add, apply hfa, apply hgb end example (hfa : fn_lb f a) (hgb : fn_lb g b) : fn_lb (λ x, f x + g x) (a + b) := sorry example (nnf : fn_lb f 0) (nng : fn_lb g 0) : fn_lb (λ x, f x * g x) 0 := sorry example (hfa : fn_ub f a) (hfb : fn_ub g b) (nng : fn_lb g 0) (nna : 0 ≤ a) : fn_ub (λ x, f x * g x) (a * b) := sorry end section variables {α : Type*} {R : Type*} [ordered_cancel_add_comm_monoid R] #check @add_le_add def fn_ub' (f : α → R) (a : R) : Prop := ∀ x, f x ≤ a theorem fn_ub_add {f g : α → R} {a b : R} (hfa : fn_ub' f a) (hgb : fn_ub' g b) : fn_ub' (λ x, f x + g x) (a + b) := λ x, add_le_add (hfa x) (hgb x) end example (f : ℝ → ℝ) (h : monotone f) : ∀ {a b}, a ≤ b → f a ≤ f b := h section variables (f g : ℝ → ℝ) example (mf : monotone f) (mg : monotone g) : monotone (λ x, f x + g x) := begin intros a b aleb, apply add_le_add, apply mf aleb, apply mg aleb end example (mf : monotone f) (mg : monotone g) : monotone (λ x, f x + g x) := λ a b aleb, add_le_add (mf aleb) (mg aleb) example {c : ℝ} (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := sorry example (mf : monotone f) (mg : monotone g) : monotone (λ x, f (g x)) := sorry def fn_even (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) def fn_odd (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (ef : fn_even f) (eg : fn_even g) : fn_even (λ x, f x + g x) := begin intro x, calc (λ x, f x + g x) x = f x + g x : rfl ... = f (-x) + g (-x) : by rw [ef, eg] end example (of : fn_odd f) (og : fn_odd g) : fn_even (λ x, f x * g x) := sorry example (ef : fn_even f) (og : fn_odd g) : fn_odd (λ x, f x * g x) := sorry example (ef : fn_even f) (og : fn_odd g) : fn_even (λ x, f (g x)) := sorry end section variables {α : Type*} (r s t : set α) example : s ⊆ s := by { intros x xs, exact xs } theorem subset.refl : s ⊆ s := λ x xs, xs theorem subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := sorry end section variables {α : Type*} [partial_order α] variables (s : set α) (a b : α) def set_ub (s : set α) (a : α) := ∀ x, x ∈ s → x ≤ a example (h : set_ub s a) (h' : a ≤ b) : set_ub s b := sorry end section open function example (c : ℝ) : injective (λ x, x + c) := begin intros x₁ x₂ h', exact (add_left_inj c).mp h', end example {c : ℝ} (h : c ≠ 0) : injective (λ x, c * x) := sorry variables {α : Type*} {β : Type*} {γ : Type*} variables {g : β → γ} {f : α → β} example (injg : injective g) (injf : injective f) : injective (λ x, g (f x)) := sorry end
-
-
-
@@ -1,149 +0,0 @@import data.real.basic example : ∃ x : ℝ, 2 < x ∧ x < 3 := begin use 5 / 2, norm_num end example : ∃ x : ℝ, 2 < x ∧ x < 3 := begin have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3, by norm_num, exact ⟨5 / 2, h⟩ end example : ∃ x : ℝ, 2 < x ∧ x < 3 := ⟨5 / 2, by norm_num⟩ def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def fn_has_ub (f : ℝ → ℝ) := ∃ a, fn_ub f a def fn_has_lb (f : ℝ → ℝ) := ∃ a, fn_lb f a theorem fn_ub_add {f g : ℝ → ℝ} {a b : ℝ} (hfa : fn_ub f a) (hgb : fn_ub g b) : fn_ub (λ x, f x + g x) (a + b) := λ x, add_le_add (hfa x) (hgb x) section variables {f g : ℝ → ℝ} example (ubf : fn_has_ub f) (ubg : fn_has_ub g) : fn_has_ub (λ x, f x + g x) := begin cases ubf with a ubfa, cases ubg with b ubfb, use a + b, apply fn_ub_add ubfa ubfb end example (lbf : fn_has_lb f) (lbg : fn_has_lb g) : fn_has_lb (λ x, f x + g x) := sorry example {c : ℝ} (ubf : fn_has_ub f) (h : c ≥ 0): fn_has_ub (λ x, c * f x) := sorry example (ubf : fn_has_ub f) (ubg : fn_has_ub g) : fn_has_ub (λ x, f x + g x) := begin rcases ubf with ⟨a, ubfa⟩, rcases ubg with ⟨b, ubfb⟩, exact ⟨a + b, fn_ub_add ubfa ubfb⟩ end example : fn_has_ub f → fn_has_ub g → fn_has_ub (λ x, f x + g x) := begin rintros ⟨a, ubfa⟩ ⟨b, ubfb⟩, exact ⟨a + b, fn_ub_add ubfa ubfb⟩ end example : fn_has_ub f → fn_has_ub g → fn_has_ub (λ x, f x + g x) := λ ⟨a, ubfa⟩ ⟨b, ubfb⟩, ⟨a + b, fn_ub_add ubfa ubfb⟩ end section variables {α : Type*} [comm_ring α] def sum_of_squares (x : α) := ∃ a b, x = a^2 + b^2 theorem sum_of_squares_mul {x y : α} (sosx : sum_of_squares x) (sosy : sum_of_squares y) : sum_of_squares (x * y) := begin rcases sosx with ⟨a, b, xeq⟩, rcases sosy with ⟨c, d, yeq⟩, rw [xeq, yeq], use [a*c - b*d, a*d + b*c], ring end theorem sum_of_squares_mul' {x y : α} (sosx : sum_of_squares x) (sosy : sum_of_squares y) : sum_of_squares (x * y) := begin rcases sosx with ⟨a, b, rfl⟩, rcases sosy with ⟨c, d, rfl⟩, use [a*c - b*d, a*d + b*c], ring end end section variables {a b c : ℕ} example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := begin cases divab with d beq, cases divbc with e ceq, rw [ceq, beq], use (d * e), ring end example (divab : a ∣ b) (divac : a ∣ c) : a ∣ (b + c) := sorry end section open function example {c : ℝ} : surjective (λ x, x + c) := begin intro x, use x - c, dsimp, ring end example {c : ℝ} (h : c ≠ 0) : surjective (λ x, c * x) := sorry example (x y : ℝ) (h : x - y ≠ 0) : (x^2 - y^2) / (x - y) = x + y := by { field_simp [h], ring } example {f : ℝ → ℝ} (h : surjective f) : ∃ x, (f x)^2 = 4 := begin cases h 2 with x hx, use x, rw hx, norm_num end end section open function variables {α : Type*} {β : Type*} {γ : Type*} variables {g : β → γ} {f : α → β} example (surjg : surjective g) (surjf : surjective f) : surjective (λ x, g (f x)) := sorry end
-
-
src/03_Logic/03_Negation.lean (deleted)
-
@@ -1,159 +0,0 @@import data.real.basic section variables a b : ℝ example (h : a < b) : ¬ b < a := begin intro h', have : a < a, from lt_trans h h', apply lt_irrefl a this end def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def fn_has_ub (f : ℝ → ℝ) := ∃ a, fn_ub f a def fn_has_lb (f : ℝ → ℝ) := ∃ a, fn_lb f a variable f : ℝ → ℝ example (h : ∀ a, ∃ x, f x > a) : ¬ fn_has_ub f := begin intros fnub, cases fnub with a fnuba, cases h a with x hx, have : f x ≤ a, from fnuba x, linarith end example (h : ∀ a, ∃ x, f x < a) : ¬ fn_has_lb f := sorry example : ¬ fn_has_ub (λ x, x) := sorry #check (not_le_of_gt : a > b → ¬ a ≤ b) #check (not_lt_of_ge : a ≥ b → ¬ a < b) #check (lt_of_not_ge : ¬ a ≥ b → a < b) #check (le_of_not_gt : ¬ a > b → a ≤ b) example (h : monotone f) (h' : f a < f b) : a < b := sorry example (h : a ≤ b) (h' : f b < f a) : ¬ monotone f := sorry example : ¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := begin intro h, let f := λ x : ℝ, (0 : ℝ), have monof : monotone f, { sorry }, have h' : f 1 ≤ f 0, from le_refl _, sorry end example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := sorry end section variables {α : Type*} (P : α → Prop) (Q : Prop) example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := sorry example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := sorry example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := sorry example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := sorry open_locale classical example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := begin by_contradiction h', apply h, intro x, show P x, by_contradiction h'', exact h' ⟨x, h''⟩ end example (h : ¬ ¬ Q) : Q := sorry example (h : Q) : ¬ ¬ Q := sorry end open_locale classical section variable (f : ℝ → ℝ) example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a := sorry example (h : ¬ ∀ a, ∃ x, f x > a) : fn_has_ub f := begin push_neg at h, exact h end example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a := begin simp only [fn_has_ub, fn_ub] at h, push_neg at h, exact h end example (h : ¬ monotone f) : ∃ x y, x ≤ y ∧ f y < f x := sorry example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a := begin contrapose! h, exact h end example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := begin contrapose! h, use x / 2, split; linarith end end section variable a : ℕ example (h : 0 < 0) : a > 37 := begin exfalso, apply lt_irrefl 0 h end example (h : 0 < 0) : a > 37 := absurd h (lt_irrefl 0) example (h : 0 < 0) : a > 37 := begin have h' : ¬ 0 < 0, from lt_irrefl 0, contradiction end end
-
-
-
@@ -1,163 +0,0 @@import data.real.basic import data.nat.prime example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := begin split, { assumption }, intro h, apply h₁, rw h end example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := ⟨h₀, λ h, h₁ (by rw h)⟩ example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := begin have h : x ≠ y, { contrapose! h₁, rw h₁ }, exact ⟨h₀, h⟩ end example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := begin cases h with h₀ h₁, contrapose! h₁, exact le_antisymm h₀ h₁ end example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬ y ≤ x := begin rintros ⟨h₀, h₁⟩ h', exact h₁ (le_antisymm h₀ h') end example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬ y ≤ x := λ ⟨h₀, h₁⟩ h', h₁ (le_antisymm h₀ h') example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := begin intro h', apply h.right, exact le_antisymm h.left h' end example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x := λ h', h.right (le_antisymm h.left h') example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := sorry example : ∃ x : ℝ, 2 < x ∧ x < 4 := ⟨5/2, by norm_num, by norm_num⟩ example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := begin rintros ⟨z, xltz, zlty⟩, exact lt_trans xltz zlty end example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := λ ⟨z, xltz, zlty⟩, lt_trans xltz zlty example : ∃ x : ℝ, 2 < x ∧ x < 4 := begin use 5 / 2, split; norm_num end example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ nat.prime m ∧ nat.prime n := begin use [5, 7], norm_num end example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := begin rintros ⟨h₀, h₁⟩, use [h₀, λ h', h₁ (le_antisymm h₀ h')] end example {x y : ℝ} (h : x ≤ y) : ¬ y ≤ x ↔ x ≠ y := begin split, { contrapose!, rintro rfl, reflexivity }, contrapose!, exact le_antisymm h end example {x y : ℝ} (h : x ≤ y) : ¬ y ≤ x ↔ x ≠ y := ⟨λ h₀ h₁, h₀ (by rw h₁), λ h₀ h₁, h₀ (le_antisymm h h₁)⟩ example {x y : ℝ} : x ≤ y ∧ ¬ y ≤ x ↔ x ≤ y ∧ x ≠ y := sorry theorem aux {x y : ℝ} (h : x^2 + y^2 = 0) : x = 0 := begin have h' : x^2 = 0, { sorry }, exact pow_eq_zero h' end example (x y : ℝ) : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := sorry section example (x y : ℝ) : abs (x + 3) < 5 → -8 < x ∧ x < 2 := begin rw abs_lt, intro h, split; linarith end example : 3 ∣ nat.gcd 6 15 := begin rw nat.dvd_gcd_iff, split; norm_num end end theorem not_monotone_iff {f : ℝ → ℝ}: ¬ monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by { rw monotone, push_neg } example : ¬ monotone (λ x : ℝ, -x) := sorry section variables {α : Type*} [partial_order α] variables a b : α example : a < b ↔ a ≤ b ∧ a ≠ b := begin rw lt_iff_le_not_le, sorry end end section variables {α : Type*} [preorder α] variables a b c : α example : ¬ a < a := begin rw lt_iff_le_not_le, sorry end example : a < b → b < c → a < c := begin simp only [lt_iff_le_not_le], sorry end end
-
-
src/03_Logic/05_Disjunction.lean (deleted)
-
@@ -1,108 +0,0 @@import data.real.basic section variables {x y : ℝ} example (h : y > x^2) : y > 0 ∨ y < -1 := by { left, linarith [pow_two_nonneg x] } example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by { right, linarith [pow_two_nonneg x] } example (h : y > 0) : y > 0 ∨ y < -1 := or.inl h example (h : y < -1) : y > 0 ∨ y < -1 := or.inr h example : x < abs y → x < y ∨ x < -y := begin cases le_or_gt 0 y with h h, { rw abs_of_nonneg h, intro h, left, exact h }, rw abs_of_neg h, intro h, right, exact h end namespace my_abs theorem le_abs_self (x : ℝ) : x ≤ abs x := sorry theorem neg_le_abs_self (x : ℝ) : -x ≤ abs x := sorry theorem abs_add (x y : ℝ) : abs (x + y) ≤ abs x + abs y := sorry theorem lt_abs : x < abs y ↔ x < y ∨ x < -y := sorry theorem abs_lt : abs x < y ↔ - y < x ∧ x < y := sorry end my_abs end example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := begin rcases lt_trichotomy x 0 with xlt | xeq | xgt, { left, exact xlt }, { contradiction }, right, exact xgt end example {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := begin rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩, { rw [mul_assoc], apply dvd_mul_right }, rw [mul_comm, mul_assoc], apply dvd_mul_right end example {z : ℝ} (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := sorry example {x : ℝ} (h : x^2 = 1) : x = 1 ∨ x = -1 := sorry example {x y : ℝ} (h : x^2 = y^2) : x = y ∨ x = -y := sorry section variables {R : Type*} [comm_ring R] [is_domain R] variables (x y : R) example (h : x^2 = 1) : x = 1 ∨ x = -1 := sorry example (h : x^2 = y^2) : x = y ∨ x = -y := sorry end example (P : Prop) : ¬ ¬ P → P := begin intro h, cases classical.em P, { assumption }, contradiction end section open_locale classical example (P : Prop) : ¬ ¬ P → P := begin intro h, by_cases h' : P, { assumption }, contradiction end example (P Q : Prop) : (P → Q) ↔ ¬ P ∨ Q := sorry end
-
-
-
@@ -1,119 +0,0 @@import data.real.basic def converges_to (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, abs (s n - a) < ε example : (λ x y : ℝ, (x + y)^2) = (λ x y : ℝ, x^2 + 2*x*y + y^2) := by { ext, ring } example (a b : ℝ) : abs a = abs (a - b + b) := by { congr, ring } example {a : ℝ} (h : 1 < a) : a < a * a := begin convert (mul_lt_mul_right _).2 h, { rw [one_mul] }, exact lt_trans zero_lt_one h end theorem converges_to_const (a : ℝ) : converges_to (λ x : ℕ, a) a := begin intros ε εpos, use 0, intros n nge, dsimp, rw [sub_self, abs_zero], apply εpos end theorem converges_to_add {s t : ℕ → ℝ} {a b : ℝ} (cs : converges_to s a) (ct : converges_to t b): converges_to (λ n, s n + t n) (a + b) := begin intros ε εpos, dsimp, have ε2pos : 0 < ε / 2, { linarith }, cases cs (ε / 2) ε2pos with Ns hs, cases ct (ε / 2) ε2pos with Nt ht, use max Ns Nt, sorry end theorem converges_to_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : converges_to s a) : converges_to (λ n, c * s n) (c * a) := begin by_cases h : c = 0, { convert converges_to_const 0, { ext, rw [h, zero_mul] }, rw [h, zero_mul] }, have acpos : 0 < abs c, from abs_pos.mpr h, sorry end theorem exists_abs_le_of_converges_to {s : ℕ → ℝ} {a : ℝ} (cs : converges_to s a) : ∃ N b, ∀ n, N ≤ n → abs (s n) < b := begin cases cs 1 zero_lt_one with N h, use [N, abs a + 1], sorry end lemma aux {s t : ℕ → ℝ} {a : ℝ} (cs : converges_to s a) (ct : converges_to t 0) : converges_to (λ n, s n * t n) 0 := begin intros ε εpos, dsimp, rcases exists_abs_le_of_converges_to cs with ⟨N₀, B, h₀⟩, have Bpos : 0 < B, from lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _)), have pos₀ : ε / B > 0, from div_pos εpos Bpos, cases ct _ pos₀ with N₁ h₁, sorry end theorem converges_to_mul {s t : ℕ → ℝ} {a b : ℝ} (cs : converges_to s a) (ct : converges_to t b): converges_to (λ n, s n * t n) (a * b) := begin have h₁ : converges_to (λ n, s n * (t n - b)) 0, { apply aux cs, convert converges_to_add ct (converges_to_const (-b)), ring }, convert (converges_to_add h₁ (converges_to_mul_const b cs)), { ext, ring }, ring end theorem converges_to_unique {s : ℕ → ℝ} {a b : ℝ} (sa : converges_to s a) (sb : converges_to s b) : a = b := begin by_contradiction abne, have : abs (a - b) > 0, { sorry }, let ε := abs (a - b) / 2, have εpos : ε > 0, { change abs (a - b) / 2 > 0, linarith }, cases sa ε εpos with Na hNa, cases sb ε εpos with Nb hNb, let N := max Na Nb, have absa : abs (s N - a) < ε, { sorry }, have absb : abs (s N - b) < ε, { sorry }, have : abs (a - b) < abs (a - b), { sorry }, exact lt_irrefl _ this end section variables {α : Type*} [linear_order α] def converges_to' (s : α → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, abs (s n - a) < ε end
-
-
-
@@ -1,151 +0,0 @@import data.real.basic def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x section variables (f g : ℝ → ℝ) (a b : ℝ) example (hfa : fn_lb f a) (hgb : fn_lb g b) : fn_lb (λ x, f x + g x) (a + b) := begin intro x, apply add_le_add, apply hfa, apply hgb end example (nnf : fn_lb f 0) (nng : fn_lb g 0) : fn_lb (λ x, f x * g x) 0 := begin intro x, apply mul_nonneg, apply nnf, apply nng end example (hfa : fn_ub f a) (hfb : fn_ub g b) (nng : fn_lb g 0) (nna : 0 ≤ a) : fn_ub (λ x, f x * g x) (a * b) := begin intro x, apply mul_le_mul, apply hfa, apply hfb, apply nng, apply nna end end section variables (f g : ℝ → ℝ) example {c : ℝ} (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := begin intros a b aleb, apply mul_le_mul_of_nonneg_left _ nnc, apply mf aleb end example {c : ℝ} (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := λ a b aleb, mul_le_mul_of_nonneg_left (mf aleb) nnc example (mf : monotone f) (mg : monotone g) : monotone (λ x, f (g x)) := begin intros a b aleb, apply mf, apply mg, apply aleb end example (mf : monotone f) (mg : monotone g) : monotone (λ x, f (g x)) := λ a b aleb, mf (mg aleb) def fn_even (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) def fn_odd (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (of : fn_odd f) (og : fn_odd g) : fn_even (λ x, f x * g x) := begin intro x, calc (λ x, f x * g x) x = f x * g x : rfl ... = f (- x) * g (- x) : by rw [of, og, neg_mul_neg] end example (ef : fn_even f) (og : fn_odd g) : fn_odd (λ x, f x * g x) := begin intro x, dsimp, rw [ef, og, neg_mul_eq_mul_neg] end example (ef : fn_even f) (og : fn_odd g) : fn_even (λ x, f (g x)) := begin intro x, dsimp, rw [og, ←ef] end end section variables {α : Type*} (r s t : set α) example : r ⊆ s → s ⊆ t → r ⊆ t := begin intros rsubs ssubt x xr, apply ssubt, apply rsubs, apply xr end theorem subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := λ rsubs ssubt x xr, ssubt (rsubs xr) end section variables {α : Type*} [partial_order α] variables (s : set α) (a b : α) def set_ub (s : set α) (a : α) := ∀ x, x ∈ s → x ≤ a example (h : set_ub s a) (h' : a ≤ b) : set_ub s b := begin intros x xs, apply le_trans (h x xs) h' end example (h : set_ub s a) (h' : a ≤ b) : set_ub s b := λ x xs, le_trans (h x xs) h' end section open function example {c : ℝ} (h : c ≠ 0) : injective (λ x, c * x) := begin intros x₁ x₂ h', apply (mul_right_inj' h).mp h' end variables {α : Type*} {β : Type*} {γ : Type*} variables {g : β → γ} {f : α → β} example (injg : injective g) (injf : injective f) : injective (λ x, g (f x)) := begin intros x₁ x₂ h, apply injf, apply injg, apply h end end
-
-
-
@@ -1,90 +0,0 @@import data.real.basic def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def fn_has_ub (f : ℝ → ℝ) := ∃ a, fn_ub f a def fn_has_lb (f : ℝ → ℝ) := ∃ a, fn_lb f a theorem fn_ub_add {f g : ℝ → ℝ} {a b : ℝ} (hfa : fn_ub f a) (hgb : fn_ub g b) : fn_ub (λ x, f x + g x) (a + b) := λ x, add_le_add (hfa x) (hgb x) section variables {f g : ℝ → ℝ} example (lbf : fn_has_lb f) (lbg : fn_has_lb g) : fn_has_lb (λ x, f x + g x) := begin cases lbf with a lbfa, cases lbg with b lbgb, use a + b, intro x, exact add_le_add (lbfa x) (lbgb x) end example {c : ℝ} (ubf : fn_has_ub f) (h : c ≥ 0): fn_has_ub (λ x, c * f x) := begin cases ubf with a lbfa, use c * a, intro x, exact mul_le_mul_of_nonneg_left (lbfa x) h end end section variables {a b c : ℕ} example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := begin rcases divab with ⟨d, rfl⟩, rcases divbc with ⟨e, rfl⟩, use (d * e), ring end example (divab : a ∣ b) (divac : a ∣ c) : a ∣ (b + c) := begin rcases divab with ⟨d, rfl⟩, rcases divac with ⟨e, rfl⟩, use (d + e), ring end end section open function example {c : ℝ} (h : c ≠ 0) : surjective (λ x, c * x) := begin intro x, use x / c, dsimp, rw [mul_div_cancel' _ h] end example {c : ℝ} (h : c ≠ 0) : surjective (λ x, c * x) := begin intro x, use x / c, field_simp [h], ring end end section open function variables {α : Type*} {β : Type*} {γ : Type*} variables {g : β → γ} {f : α → β} example (surjg : surjective g) (surjf : surjective f) : surjective (λ x, g (f x)) := begin intro z, rcases surjg z with ⟨y, rfl⟩, rcases surjf y with ⟨x, rfl⟩, use [x, rfl] end end
-
-
-
@@ -1,132 +0,0 @@import data.real.basic section variables a b : ℝ def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def fn_has_ub (f : ℝ → ℝ) := ∃ a, fn_ub f a def fn_has_lb (f : ℝ → ℝ) := ∃ a, fn_lb f a variable f : ℝ → ℝ example (h : ∀ a, ∃ x, f x < a) : ¬ fn_has_lb f := begin rintros ⟨a, ha⟩, rcases h a with ⟨x, hx⟩, have := ha x, linarith end example : ¬ fn_has_ub (λ x, x) := begin rintros ⟨a, ha⟩, have : a + 1 ≤ a := ha (a + 1), linarith end example (h : monotone f) (h' : f a < f b) : a < b := begin apply lt_of_not_ge, intro h'', apply absurd h', apply not_lt_of_ge (h h'') end example (h : a ≤ b) (h' : f b < f a) : ¬ monotone f := begin intro h'', apply absurd h', apply not_lt_of_ge, apply h'' h end example : ¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := begin intro h, let f := λ x : ℝ, (0 : ℝ), have monof : monotone f, { intros a b leab, refl }, have h' : f 1 ≤ f 0, from le_refl _, have : (1 : ℝ) ≤ 0 := h monof h', linarith end example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := begin apply le_of_not_gt, intro h', linarith [h _ h'] end end section variables {α : Type*} (P : α → Prop) (Q : Prop) example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x := begin intros x Px, apply h, use [x, Px] end example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x := begin rintros ⟨x, Px⟩, exact h x Px end example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x := begin intro h', rcases h with ⟨x, nPx⟩, apply nPx, apply h' end example (h : ¬ ¬ Q) : Q := begin by_contradiction h', exact h h' end example (h : Q) : ¬ ¬ Q := begin intro h', exact h' h end end open_locale classical section variable (f : ℝ → ℝ) example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a := begin intro a, by_contradiction h', apply h, use a, intro x, apply le_of_not_gt, intro h'', apply h', use [x, h''] end example (h : ¬ monotone f) : ∃ x y, x ≤ y ∧ f y < f x := begin rw [monotone] at h, push_neg at h, exact h end end
-
-
-
@@ -1,108 +0,0 @@import data.real.basic import data.nat.prime example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := begin cases h with h0 h1, split, { exact h0 }, intro h2, apply h1, apply nat.dvd_antisymm h0 h2, end example {x y : ℝ} : x ≤ y ∧ ¬ y ≤ x ↔ x ≤ y ∧ x ≠ y := begin split, { rintros ⟨h0, h1⟩, split, { exact h0 }, intro h2, apply h1, rw h2 }, rintros ⟨h0, h1⟩, split, { exact h0 }, intro h2, apply h1, apply le_antisymm h0 h2 end theorem aux {x y : ℝ} (h : x^2 + y^2 = 0) : x = 0 := begin have h' : x^2 = 0, { linarith [pow_two_nonneg x, pow_two_nonneg y] }, exact pow_eq_zero h' end example (x y : ℝ) : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := begin split, { intro h, split, { exact aux h }, rw add_comm at h, exact aux h }, rintros ⟨rfl, rfl⟩, norm_num end theorem not_monotone_iff {f : ℝ → ℝ}: ¬ monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by { rw monotone, push_neg } example : ¬ monotone (λ x : ℝ, -x) := begin rw not_monotone_iff, use [0, 1], norm_num end section variables {α : Type*} [partial_order α] variables a b : α example : a < b ↔ a ≤ b ∧ a ≠ b := begin rw lt_iff_le_not_le, split, { rintros ⟨h0, h1⟩, split, { exact h0 }, intro h2, apply h1, rw h2 }, rintros ⟨h0, h1⟩, split, { exact h0 }, intro h2, apply h1, apply le_antisymm h0 h2 end end section variables {α : Type*} [preorder α] variables a b c : α example : ¬ a < a := begin rw lt_iff_le_not_le, rintros ⟨h0, h1⟩, exact h1 h0 end example : a < b → b < c → a < c := begin simp only [lt_iff_le_not_le], rintros ⟨h0, h1⟩ ⟨h2, h3⟩, split, { apply le_trans h0 h2 }, intro h4, apply h1, apply le_trans h2 h4 end end
-
-
-
@@ -1,162 +0,0 @@import data.real.basic section variables {x y : ℝ} namespace my_abs theorem le_abs_self (x : ℝ) : x ≤ abs x := begin cases le_or_gt 0 x with h h, { rw abs_of_nonneg h }, rw abs_of_neg h, linarith end theorem neg_le_abs_self (x : ℝ) : -x ≤ abs x := begin cases le_or_gt 0 x with h h, { rw abs_of_nonneg h, linarith }, rw abs_of_neg h end theorem abs_add (x y : ℝ) : abs (x + y) ≤ abs x + abs y := begin cases le_or_gt 0 (x + y) with h h, { rw abs_of_nonneg h, linarith [le_abs_self x, le_abs_self y] }, rw abs_of_neg h, linarith [neg_le_abs_self x, neg_le_abs_self y] end theorem lt_abs : x < abs y ↔ x < y ∨ x < -y := begin cases le_or_gt 0 y with h h, { rw abs_of_nonneg h, split, { intro h', left, exact h' }, intro h', cases h' with h' h', { exact h' }, linarith }, rw abs_of_neg h, split, { intro h', right, exact h' }, intro h', cases h' with h' h', { linarith }, exact h' end theorem abs_lt : abs x < y ↔ - y < x ∧ x < y := begin cases le_or_gt 0 x with h h, { rw abs_of_nonneg h, split, { intro h', split, { linarith }, exact h' }, intro h', cases h' with h1 h2, exact h2 }, rw abs_of_neg h, split, { intro h', split, { linarith }, linarith }, intro h', linarith end end my_abs end example {z : ℝ} (h : ∃ x y, z = x^2 + y^2 ∨ z = x^2 + y^2 + 1) : z ≥ 0 := by { rcases h with ⟨x, y, rfl | rfl⟩; linarith [sq_nonneg x, sq_nonneg y] } example {x : ℝ} (h : x^2 = 1) : x = 1 ∨ x = -1 := begin have h' : x^2 - 1 = 0, { rw [h, sub_self] }, have h'' : (x + 1) * (x - 1) = 0, { rw ← h', ring }, cases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 h1, { right, exact eq_neg_iff_add_eq_zero.mpr h1 }, left, exact eq_of_sub_eq_zero h1 end example {x y : ℝ} (h : x^2 = y^2) : x = y ∨ x = -y := begin have h' : x^2 - y^2 = 0, { rw [h, sub_self] }, have h'' : (x + y) * (x - y) = 0, { rw ← h', ring }, cases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 h1, { right, exact eq_neg_iff_add_eq_zero.mpr h1 }, left, exact eq_of_sub_eq_zero h1 end section variables {R : Type*} [comm_ring R] [is_domain R] variables (x y : R) example (h : x^2 = 1) : x = 1 ∨ x = -1 := begin have h' : x^2 - 1 = 0, { rw [h, sub_self] }, have h'' : (x + 1) * (x - 1) = 0, { rw ← h', ring }, cases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 h1, { right, exact eq_neg_iff_add_eq_zero.mpr h1 }, left, exact eq_of_sub_eq_zero h1 end example (h : x^2 = y^2) : x = y ∨ x = -y := begin have h' : x^2 - y^2 = 0, { rw [h, sub_self] }, have h'' : (x + y) * (x - y) = 0, { rw ← h', ring }, cases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 h1, { right, exact eq_neg_iff_add_eq_zero.mpr h1 }, left, exact eq_of_sub_eq_zero h1 end end section open_locale classical example (P Q : Prop) : (P → Q) ↔ ¬ P ∨ Q := begin split, { intro h, by_cases h' : P, { right, exact h h'}, left, exact h' }, rintros (h | h), { intro h', exact absurd h' h }, intro _, exact h end end
-
-
-
@@ -1,143 +0,0 @@import data.real.basic def converges_to (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, abs (s n - a) < ε theorem converges_to_const (a : ℝ) : converges_to (λ x : ℕ, a) a := begin intros ε εpos, use 0, intros n nge, dsimp, rw [sub_self, abs_zero], apply εpos end theorem converges_to_add {s t : ℕ → ℝ} {a b : ℝ} (cs : converges_to s a) (ct : converges_to t b): converges_to (λ n, s n + t n) (a + b) := begin intros ε εpos, dsimp, have ε2pos : 0 < ε / 2, { linarith }, cases cs (ε / 2) ε2pos with Ns hs, cases ct (ε / 2) ε2pos with Nt ht, use max Ns Nt, intros n hn, have ngeNs : n ≥ Ns := le_of_max_le_left hn, have ngeNt : n ≥ Nt := le_of_max_le_right hn, calc |s n + t n - (a + b)| = | s n - a + (t n - b) | : by { congr, ring } ... ≤ | s n - a | + | (t n - b) | : abs_add _ _ ... < ε / 2 + ε / 2 : add_lt_add (hs n ngeNs) (ht n ngeNt) ... = ε : by norm_num end theorem converges_to_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : converges_to s a) : converges_to (λ n, c * s n) (c * a) := begin by_cases h : c = 0, { convert converges_to_const 0, { ext, rw [h, zero_mul] }, rw [h, zero_mul] }, have acpos : 0 < abs c, from abs_pos.mpr h, intros ε εpos, dsimp, have εcpos : 0 < ε / abs c, { apply div_pos εpos acpos }, cases cs (ε / abs c) εcpos with Ns hs, use Ns, intros n ngt, calc |c * s n - c * a| = |c| * |s n - a| : by { rw [←abs_mul, mul_sub] } ... < |c| * (ε / |c|) : mul_lt_mul_of_pos_left (hs n ngt) acpos ... = ε : mul_div_cancel' _ (ne_of_lt acpos).symm end theorem exists_abs_le_of_converges_to {s : ℕ → ℝ} {a : ℝ} (cs : converges_to s a) : ∃ N b, ∀ n, N ≤ n → abs (s n) < b := begin cases cs 1 zero_lt_one with N h, use [N, abs a + 1], intros n ngt, calc |s n| = |s n - a + a| : by { congr, abel } ... ≤ |s n - a| + |a| : abs_add _ _ ... < |a| + 1 : by linarith [h n ngt] end lemma aux {s t : ℕ → ℝ} {a : ℝ} (cs : converges_to s a) (ct : converges_to t 0) : converges_to (λ n, s n * t n) 0 := begin intros ε εpos, dsimp, rcases exists_abs_le_of_converges_to cs with ⟨N₀, B, h₀⟩, have Bpos : 0 < B, from lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _)), have pos₀ : ε / B > 0, from div_pos εpos Bpos, cases ct _ pos₀ with N₁ h₁, use max N₀ N₁, intros n ngt, have ngeN₀ : n ≥ N₀ := le_of_max_le_left ngt, have ngeN₁ : n ≥ N₁ := le_of_max_le_right ngt, calc |s n * t n - 0| = |s n| * |t n - 0| : by rw [sub_zero, abs_mul, sub_zero] ... < B * (ε / B) : mul_lt_mul'' (h₀ n ngeN₀) (h₁ n ngeN₁) (abs_nonneg _) (abs_nonneg _) ... = ε : mul_div_cancel' _ (ne_of_lt Bpos).symm end theorem converges_to_muL {s t : ℕ → ℝ} {a b : ℝ} (cs : converges_to s a) (ct : converges_to t b): converges_to (λ n, s n * t n) (a * b) := begin have h₁ : converges_to (λ n, s n * (t n - b)) 0, { apply aux cs, convert converges_to_add ct (converges_to_const (-b)), ring }, convert (converges_to_add h₁ (converges_to_mul_const b cs)), { ext, ring }, ring end theorem converges_to_unique {s : ℕ → ℝ} {a b : ℝ} (sa : converges_to s a) (sb : converges_to s b) : a = b := begin by_contradiction abne, have : abs (a - b) > 0, { apply lt_of_le_of_ne, { apply abs_nonneg }, intro h'', apply abne, apply eq_of_abs_sub_eq_zero h''.symm, }, let ε := abs (a - b) / 2, have εpos : ε > 0, { change abs (a - b) / 2 > 0, linarith }, cases sa ε εpos with Na hNa, cases sb ε εpos with Nb hNb, let N := max Na Nb, have absa : abs (s N - a) < ε, { apply hNa, apply le_max_left }, have absb : abs (s N - b) < ε, { apply hNb, apply le_max_right }, have : abs (a - b) < abs (a - b), calc abs (a - b) = abs (- (s N - a) + (s N - b)) : by { congr, ring } ... ≤ abs (- (s N - a)) + abs (s N - b) : abs_add _ _ ... = abs (s N - a) + abs (s N - b) : by rw [abs_neg] ... < ε + ε : add_lt_add absa absb ... = abs (a - b) : by norm_num, exact lt_irrefl _ this end
-
-
src/04_Sets_and_Functions/01_Sets.lean (deleted)
-
@@ -1,273 +0,0 @@import data.set.lattice import data.nat.parity import tactic section variable {α : Type*} variables (s t u : set α) open set example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin rw [subset_def, inter_def, inter_def], rw subset_def at h, dsimp, rintros x ⟨xs, xu⟩, exact ⟨h _ xs, xu⟩, end example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin simp only [subset_def, mem_inter_eq] at *, rintros x ⟨xs, xu⟩, exact ⟨h _ xs, xu⟩, end example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin intros x xsu, exact ⟨h xsu.1, xsu.2⟩ end theorem foo (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := λ x ⟨xs, xu⟩, ⟨h xs, xu⟩ example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by exact λ x ⟨xs, xu⟩, ⟨h xs, xu⟩ example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := begin intros x hx, have xs : x ∈ s := hx.1, have xtu : x ∈ t ∪ u := hx.2, cases xtu with xt xu, { left, show x ∈ s ∩ t, exact ⟨xs, xt⟩ }, right, show x ∈ s ∩ u, exact ⟨xs, xu⟩ end example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := begin rintros x ⟨xs, xt | xu⟩, { left, exact ⟨xs, xt⟩ }, right, exact ⟨xs, xu⟩ end example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= sorry example : s \ t \ u ⊆ s \ (t ∪ u) := begin intros x xstu, have xs : x ∈ s := xstu.1.1, have xnt : x ∉ t := xstu.1.2, have xnu : x ∉ u := xstu.2, split, { exact xs }, dsimp, intro xtu, -- x ∈ t ∨ x ∈ u cases xtu with xt xu, { show false, from xnt xt }, show false, from xnu xu end example : s \ t \ u ⊆ s \ (t ∪ u) := begin rintros x ⟨⟨xs, xnt⟩, xnu⟩, use xs, rintros (xt | xu); contradiction end example : s \ (t ∪ u) ⊆ s \ t \ u := sorry example : s ∩ t = t ∩ s := begin ext x, simp only [mem_inter_eq], split, { rintros ⟨xs, xt⟩, exact ⟨xt, xs⟩ }, rintros ⟨xt, xs⟩, exact ⟨xs, xt⟩ end example : s ∩ t = t ∩ s := set.ext $ λ x, ⟨λ ⟨xs, xt⟩, ⟨xt, xs⟩, λ ⟨xt, xs⟩, ⟨xs, xt⟩⟩ example : s ∩ t = t ∩ s := by ext x; simp [and.comm] example : s ∩ t = t ∩ s := begin apply subset.antisymm, { rintros x ⟨xs, xt⟩, exact ⟨xt, xs⟩ }, rintros x ⟨xt, xs⟩, exact ⟨xs, xt⟩ end example : s ∩ t = t ∩ s := subset.antisymm sorry sorry example : s ∩ (s ∪ t) = s := sorry example : s ∪ (s ∩ t) = s := sorry example : (s \ t) ∪ t = s ∪ t := sorry example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) := sorry def evens : set ℕ := {n | even n} def odds : set ℕ := {n | ¬ even n} example : evens ∪ odds = univ := begin rw [evens, odds], ext n, simp, apply classical.em end example (x : ℕ) (h : x ∈ (∅ : set ℕ)) : false := h example (x : ℕ) : x ∈ (univ : set ℕ) := trivial example : { n | nat.prime n } ∩ { n | n > 2} ⊆ { n | ¬ even n } := sorry #print prime #print nat.prime example (n : ℕ) : prime n ↔ nat.prime n := nat.prime_iff.symm example (n : ℕ) (h : prime n) : nat.prime n := by { rw nat.prime_iff, exact h } example (n : ℕ) (h : prime n) : nat.prime n := by rwa nat.prime_iff end section variables (s t : set ℕ) example (h₀ : ∀ x ∈ s, ¬ even x) (h₁ : ∀ x ∈ s, prime x) : ∀ x ∈ s, ¬ even x ∧ prime x := begin intros x xs, split, { apply h₀ x xs }, apply h₁ x xs end example (h : ∃ x ∈ s, ¬ even x ∧ prime x) : ∃ x ∈ s, prime x := begin rcases h with ⟨x, xs, _, prime_x⟩, use [x, xs, prime_x] end section variable (ssubt : s ⊆ t) include ssubt example (h₀ : ∀ x ∈ t, ¬ even x) (h₁ : ∀ x ∈ t, prime x) : ∀ x ∈ s, ¬ even x ∧ prime x := sorry example (h : ∃ x ∈ s, ¬ even x ∧ prime x) : ∃ x ∈ t, prime x := sorry end end section variables {α I : Type*} variables A B : I → set α variable s : set α open set example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := begin ext x, simp only [mem_inter_eq, mem_Union], split, { rintros ⟨xs, ⟨i, xAi⟩⟩, exact ⟨i, xAi, xs⟩ }, rintros ⟨i, xAi, xs⟩, exact ⟨xs, ⟨i, xAi⟩⟩ end example : (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) := begin ext x, simp only [mem_inter_eq, mem_Inter], split, { intro h, split, { intro i, exact (h i).1 }, intro i, exact (h i).2 }, rintros ⟨h1, h2⟩ i, split, { exact h1 i }, exact h2 i end open_locale classical example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) := sorry def primes : set ℕ := {x | nat.prime x} example : (⋃ p ∈ primes, {x | p^2 ∣ x}) = {x | ∃ p ∈ primes, p^2 ∣ x} := by { ext, rw mem_Union₂, refl } example : (⋃ p ∈ primes, {x | p^2 ∣ x}) = {x | ∃ p ∈ primes, p^2 ∣ x} := by { ext, simp } example : (⋂ p ∈ primes, {x | ¬ p ∣ x}) ⊆ {x | x = 1} := begin intro x, contrapose!, simp, apply nat.exists_prime_and_dvd end example : (⋃ p ∈ primes, {x | x ≤ p}) = univ := sorry end section open set variables {α : Type*} (s : set (set α)) example : ⋃₀ s = ⋃ t ∈ s, t := begin ext x, rw mem_Union₂, refl end example : ⋂₀ s = ⋂ t ∈ s, t := begin ext x, rw mem_Inter₂, refl end end
-
-
-
@@ -1,216 +0,0 @@import data.set.lattice import data.set.function import analysis.special_functions.log.basic section variables {α β : Type*} variable f : α → β variables s t : set α variables u v : set β open function open set example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by { ext, refl } example : f '' (s ∪ t) = f '' s ∪ f '' t := begin ext y, split, { rintros ⟨x, xs | xt, rfl⟩, { left, use [x, xs] }, right, use [x, xt] }, rintros (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩), { use [x, or.inl xs] }, use [x, or.inr xt] end example : s ⊆ f ⁻¹' (f '' s) := begin intros x xs, show f x ∈ f '' s, use [x, xs] end example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v := sorry example (h : injective f) : f ⁻¹' (f '' s) ⊆ s := sorry example : f '' (f⁻¹' u) ⊆ u := sorry example (h : surjective f) : u ⊆ f '' (f⁻¹' u) := sorry example (h : s ⊆ t) : f '' s ⊆ f '' t := sorry example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := sorry example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v := sorry example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := sorry example (h : injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := sorry example : f '' s \ f '' t ⊆ f '' (s \ t) := sorry example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) := sorry example : f '' s ∩ v = f '' (s ∩ f ⁻¹' v) := sorry example : f '' (s ∩ f ⁻¹' u) ⊆ f '' s ∪ u := sorry example : s ∩ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∩ u) := sorry example : s ∪ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∪ u) := sorry variables {I : Type*} (A : I → set α) (B : I → set β) example : f '' (⋃ i, A i) = ⋃ i, f '' A i := begin ext y, simp, split, { rintros ⟨x, ⟨i, xAi⟩, fxeq⟩, use [i, x, xAi, fxeq] }, rintros ⟨i, x, xAi, fxeq⟩, exact ⟨x, ⟨i, xAi⟩, fxeq⟩ end example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := begin intro y, simp, intros x h fxeq i, use [x, h i, fxeq], end example (i : I) (injf : injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := begin intro y, simp, intro h, rcases h i with ⟨x, xAi, fxeq⟩, use x, split, { intro i', rcases h i' with ⟨x', x'Ai, fx'eq⟩, have : f x = f x', by rw [fxeq, fx'eq], have : x = x', from injf this, rw this, exact x'Ai }, exact fxeq end example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) := by { ext x, simp } example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) := by { ext x, simp } end section open set real example : inj_on log { x | x > 0 } := begin intros x xpos y ypos, intro e, -- log x = log y calc x = exp (log x) : by rw exp_log xpos ... = exp (log y) : by rw e ... = y : by rw exp_log ypos end example : range exp = { y | y > 0 } := begin ext y, split, { rintros ⟨x, rfl⟩, apply exp_pos }, intro ypos, use log y, rw exp_log ypos end example : inj_on sqrt { x | x ≥ 0 } := sorry example : inj_on (λ x, x^2) { x : ℝ | x ≥ 0 } := sorry example : sqrt '' { x | x ≥ 0 } = {y | y ≥ 0} := sorry example : range (λ x, x^2) = {y : ℝ | y ≥ 0} := sorry end section variables {α β : Type*} [inhabited α] #check (default : α) variables (P : α → Prop) (h : ∃ x, P x) #check classical.some h example : P (classical.some h) := classical.some_spec h noncomputable theory open_locale classical def inverse (f : α → β) : β → α := λ y : β, if h : ∃ x, f x = y then classical.some h else default theorem inverse_spec {f : α → β} (y : β) (h : ∃ x, f x = y) : f (inverse f y) = y := begin rw inverse, dsimp, rw dif_pos h, exact classical.some_spec h end variable f : α → β open function example : injective f ↔ left_inverse (inverse f) f := sorry example : surjective f ↔ right_inverse (inverse f) f := sorry end section variable {α : Type*} open function theorem Cantor : ∀ f : α → set α, ¬ surjective f := begin intros f surjf, let S := { i | i ∉ f i}, rcases surjf S with ⟨j, h⟩, have h₁ : j ∉ f j, { intro h', have : j ∉ f j, { by rwa h at h' }, contradiction }, have h₂ : j ∈ S, sorry, have h₃ : j ∉ S, sorry, contradiction end end
-
-
-
@@ -1,108 +0,0 @@import data.set.lattice import data.set.function import tactic open set open function noncomputable theory open_locale classical variables {α β : Type*} [nonempty β] section variables (f : α → β) (g : β → α) def sb_aux : ℕ → set α | 0 := univ \ (g '' univ) | (n + 1) := g '' (f '' sb_aux n) def sb_set := ⋃ n, sb_aux f g n def sb_fun (x : α) : β := if x ∈ sb_set f g then f x else inv_fun g x theorem sb_right_inv {x : α} (hx : x ∉ sb_set f g) : g (inv_fun g x) = x := begin have : x ∈ g '' univ, { contrapose! hx, rw [sb_set, mem_Union], use [0], rw [sb_aux, mem_diff], sorry }, have : ∃ y, g y = x, { sorry }, sorry end theorem sb_injective (hf: injective f) (hg : injective g) : injective (sb_fun f g) := begin set A := sb_set f g with A_def, set h := sb_fun f g with h_def, intros x₁ x₂, assume hxeq : h x₁ = h x₂, show x₁ = x₂, simp only [h_def, sb_fun, ←A_def] at hxeq, by_cases xA : x₁ ∈ A ∨ x₂ ∈ A, { wlog : x₁ ∈ A := xA using [x₁ x₂, x₂ x₁], have x₂A : x₂ ∈ A, { apply not_imp_self.mp, assume x₂nA : x₂ ∉ A, rw [if_pos xA, if_neg x₂nA] at hxeq, rw [A_def, sb_set, mem_Union] at xA, have x₂eq : x₂ = g (f x₁), { sorry }, rcases xA with ⟨n, hn⟩, rw [A_def, sb_set, mem_Union], use n + 1, simp [sb_aux], exact ⟨x₁, hn, x₂eq.symm⟩ }, sorry }, push_neg at xA, sorry end theorem sb_surjective (hf: injective f) (hg : injective g) : surjective (sb_fun f g) := begin set A := sb_set f g with A_def, set h := sb_fun f g with h_def, intro y, by_cases gyA : g y ∈ A, { rw [A_def, sb_set, mem_Union] at gyA, rcases gyA with ⟨n, hn⟩, cases n with n, { simp [sb_aux] at hn, contradiction }, simp [sb_aux] at hn, rcases hn with ⟨x, xmem, hx⟩, use x, have : x ∈ A, { rw [A_def, sb_set, mem_Union], exact ⟨n, xmem⟩ }, simp only [h_def, sb_fun, if_pos this], exact hg hx }, sorry end end theorem schroeder_bernstein {f : α → β} {g : β → α} (hf: injective f) (hg : injective g) : ∃ h : α → β, bijective h := ⟨sb_fun f g, sb_injective f g hf hg, sb_surjective f g hf hg⟩ /- Auxliary information -/ section variables (g : β → α) (x : α) #check (inv_fun g : α → β) #check (left_inverse_inv_fun : injective g → left_inverse (inv_fun g) g) #check (left_inverse_inv_fun : injective g → ∀ y, inv_fun g (g y) = y) #check (inv_fun_eq : (∃ y, g y = x) → g (inv_fun g x) = x) end
-
-
-
@@ -1,151 +0,0 @@import data.set.lattice import data.nat.parity import tactic section variable {α : Type*} variables (s t u : set α) open set example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= begin rintros x (⟨xs, xt⟩ | ⟨xs, xu⟩), { use xs, left, exact xt }, use xs, right, exact xu end example : s \ (t ∪ u) ⊆ s \ t \ u := begin rintros x ⟨xs, xntu⟩, use xs, { intro xt, exact xntu (or.inl xt) }, intro xu, apply xntu (or.inr xu) end example : s ∩ t = t ∩ s := subset.antisymm (λ x ⟨xs, xt⟩, ⟨xt, xs⟩) (λ x ⟨xt, xs⟩, ⟨xs, xt⟩) example : s ∩ (s ∪ t) = s := begin ext x, split, { rintros ⟨xs, _⟩, exact xs }, intro xs, use xs, left, exact xs end example : s ∪ (s ∩ t) = s := begin ext x, split, { rintros (xs | ⟨xs, xt⟩); exact xs }, intro xs, left, exact xs end example : (s \ t) ∪ t = s ∪ t := begin ext x, split, { rintros (⟨xs, nxt⟩ | xt), { left, exact xs}, right, exact xt }, by_cases h : x ∈ t, { intro _, right, exact h }, rintros (xs | xt), { left, use [xs, h] }, right, use xt end example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) := begin ext x, split, { rintros (⟨xs, xnt⟩ | ⟨xt, xns⟩), { split, left, exact xs, rintros ⟨_, xt⟩, contradiction }, split , right, exact xt, rintros ⟨xs, _⟩, contradiction }, rintros ⟨xs | xt, nxst⟩, { left, use xs, intro xt, apply nxst, split; assumption }, right, use xt, intro xs, apply nxst, split; assumption end example : { n | nat.prime n } ∩ { n | n > 2} ⊆ { n | ¬ even n } := begin intro n, simp, intro nprime, cases nat.prime.eq_two_or_odd nprime with h h, { rw h, intro, linarith }, rw [nat.even_iff, h], norm_num end end section variables (s t : set ℕ) section variable (ssubt : s ⊆ t) include ssubt example (h₀ : ∀ x ∈ t, ¬ even x) (h₁ : ∀ x ∈ t, prime x) : ∀ x ∈ s, ¬ even x ∧ prime x := begin intros x xs, split, { apply h₀ x (ssubt xs) }, apply h₁ x (ssubt xs) end example (h : ∃ x ∈ s, ¬ even x ∧ prime x) : ∃ x ∈ t, prime x := begin rcases h with ⟨x, xs, _, px⟩, use [x, ssubt xs, px] end end end section variables {α I : Type*} variables A B : I → set α variable s : set α open set example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) := begin ext x, simp only [mem_union, mem_Inter], split, { rintros (xs | xI), { intro i, right, exact xs }, intro i, left, exact xI i }, intro h, by_cases xs : x ∈ s, { left, exact xs }, right, intro i, cases h i, { assumption }, contradiction end def primes : set ℕ := {x | nat.prime x} example : (⋃ p ∈ primes, {x | x ≤ p}) = univ := begin apply eq_univ_of_forall, intro x, simp, rcases nat.exists_infinite_primes x with ⟨p, primep, pge⟩, use [p, pge, primep] end end
-
-
-
@@ -1,281 +0,0 @@import data.set.lattice import data.set.function import analysis.special_functions.log.basic section variables {α β : Type*} variable f : α → β variables s t : set α variables u v : set β open function open set example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v := begin split, { intros h x xs, have : f x ∈ f '' s, from mem_image_of_mem _ xs, exact h this }, intros h y ymem, rcases ymem with ⟨x, xs, fxeq⟩, rw ← fxeq, apply h xs end example (h : injective f) : f ⁻¹' (f '' s) ⊆ s := begin rintros x ⟨y, ys, fxeq⟩, rw ← h fxeq, exact ys end example : f '' (f⁻¹' u) ⊆ u := begin rintros y ⟨x, xmem, rfl⟩, exact xmem end example (h : surjective f) : u ⊆ f '' (f⁻¹' u) := begin intros y yu, rcases h y with ⟨x, fxeq⟩, use x, split, { show f x ∈ u, rw fxeq, exact yu }, exact fxeq end example (h : s ⊆ t) : f '' s ⊆ f '' t := begin rintros y ⟨x, xs, fxeq⟩, use [x, h xs, fxeq] end example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intro x; apply h example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v := by ext x; refl example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := begin rintros y ⟨x, ⟨xs, xt⟩, rfl⟩, use [x, xs, rfl, x, xt, rfl] end example (h : injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := begin rintros y ⟨⟨x₁, x₁s, rfl⟩, ⟨x₂, x₂t, fx₂eq⟩⟩, use [x₁, x₁s], rw ← h fx₂eq, exact x₂t end example : f '' s \ f '' t ⊆ f '' (s \ t) := begin rintros y ⟨⟨x₁, x₁s, rfl⟩, h⟩, use [x₁, x₁s], intro h', apply h, use [x₁, h', rfl] end example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) := λ x, id example : f '' s ∩ v = f '' (s ∩ f ⁻¹' v) := begin ext y, split, { rintros ⟨⟨x, xs, rfl⟩, fxv⟩, use [x, xs, fxv] }, rintros ⟨x, ⟨⟨xs, fxv⟩, rfl⟩⟩, use [x, xs, rfl, fxv], end example : f '' (s ∩ f ⁻¹' u) ⊆ f '' s ∩ u := begin rintros y ⟨x, ⟨xs, fxu⟩, rfl⟩, use [x, xs, rfl, fxu], end example : s ∩ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∩ u) := begin rintros x ⟨xs, fxu⟩, use [x, xs, rfl, fxu], end example : s ∪ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∪ u) := begin rintros x (xs | fxu), { left, use [x, xs, rfl] }, right, use fxu end variables {I : Type*} (A : I → set α) (B : I → set β) example : f '' (⋃ i, A i) = ⋃ i, f '' A i := begin ext y, simp, split, { rintros ⟨x, ⟨i, xAi⟩, fxeq⟩, use [i, x, xAi, fxeq] }, rintros ⟨i, x, xAi, fxeq⟩, exact ⟨x, ⟨i, xAi⟩, fxeq⟩ end example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := begin intro y, simp, intros x h fxeq i, use [x, h i, fxeq], end example (i : I) (injf : injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := begin intro y, simp, intro h, rcases h i with ⟨x, xAi, fxeq⟩, use x, split, { intro i', rcases h i' with ⟨x', x'Ai, fx'eq⟩, have : f x = f x', by rw [fxeq, fx'eq], have : x = x', from injf this, rw this, exact x'Ai }, exact fxeq end example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) := by { ext x, simp } example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) := by { ext x, simp } end section open set real example : inj_on sqrt { x | x ≥ 0 } := begin intros x xnonneg y ynonneg, intro e, calc x = (sqrt x)^2 : by rw sq_sqrt xnonneg ... = (sqrt y)^2 : by rw e ... = y : by rw sq_sqrt ynonneg end example : inj_on (λ x, x^2) { x : ℝ | x ≥ 0 } := begin intros x xnonneg y ynonneg, intro e, dsimp at *, calc x = sqrt (x^2) : by rw sqrt_sq xnonneg ... = sqrt (y^2) : by rw e ... = y : by rw sqrt_sq ynonneg, end example : sqrt '' { x | x ≥ 0 } = {y | y ≥ 0} := begin ext y, split, { rintros ⟨x, ⟨xnonneg, rfl⟩⟩, apply sqrt_nonneg }, intro ynonneg, use y^2, dsimp at *, split, apply pow_nonneg ynonneg, apply sqrt_sq, assumption, end example : range (λ x, x^2) = {y : ℝ | y ≥ 0} := begin ext y, split, { rintros ⟨x, rfl⟩, dsimp at *, apply pow_two_nonneg }, intro ynonneg, use sqrt y, exact sq_sqrt ynonneg, end end section variables {α β : Type*} [inhabited α] noncomputable theory open_locale classical def inverse (f : α → β) : β → α := λ y : β, if h : ∃ x, f x = y then classical.some h else default theorem inverse_spec {f : α → β} (y : β) (h : ∃ x, f x = y) : f (inverse f y) = y := begin rw inverse, dsimp, rw dif_pos h, exact classical.some_spec h end variable f : α → β open function example : injective f ↔ left_inverse (inverse f) f := begin split, { intros h y, apply h, apply inverse_spec, use y }, intros h x1 x2 e, rw [←h x1, ←h x2, e] end example : injective f ↔ left_inverse (inverse f) f := ⟨λ h y, h (inverse_spec _ ⟨y, rfl⟩), λ h x1 x2 e, by rw [←h x1, ←h x2, e]⟩ example : surjective f ↔ right_inverse (inverse f) f := begin split, { intros h y, apply inverse_spec, apply h }, intros h y, use (inverse f y), apply h end example : surjective f ↔ right_inverse (inverse f) f := ⟨λ h y, inverse_spec _ (h _), λ h y, ⟨inverse f y, h _⟩⟩ end section variable {α : Type*} open function theorem Cantor : ∀ f : α → set α, ¬ surjective f := begin intros f surjf, let S := { i | i ∉ f i}, rcases surjf S with ⟨j, h⟩, have h₁ : j ∉ f j, { intro h', have : j ∉ f j, by rwa h at h', contradiction }, have h₂ : j ∈ S, from h₁, have h₃ : j ∉ S, by rwa h at h₁, contradiction end end
-
-
-
@@ -1,94 +0,0 @@import data.set.lattice import data.set.function import tactic open set open function noncomputable theory open_locale classical variables {α β : Type*} [nonempty β] section variables (f : α → β) (g : β → α) def sb_aux : ℕ → set α | 0 := univ \ (g '' univ) | (n + 1) := g '' (f '' sb_aux n) def sb_set := ⋃ n, sb_aux f g n def sb_fun (x : α) : β := if x ∈ sb_set f g then f x else inv_fun g x theorem sb_right_inv {x : α} (hx : x ∉ sb_set f g) : g (inv_fun g x) = x := begin have : x ∈ g '' univ, { contrapose! hx, rw [sb_set, mem_Union], use [0], rw [sb_aux, mem_diff], exact ⟨mem_univ _, hx⟩ }, have : ∃ y, g y = x, { simp at this, assumption }, exact inv_fun_eq this end theorem sb_injective (hf: injective f) (hg : injective g) : injective (sb_fun f g) := begin set A := sb_set f g with A_def, set h := sb_fun f g with h_def, intros x₁ x₂, assume hxeq : h x₁ = h x₂, show x₁ = x₂, simp only [h_def, sb_fun, ←A_def] at hxeq, by_cases xA : x₁ ∈ A ∨ x₂ ∈ A, { wlog : x₁ ∈ A := xA using [x₁ x₂, x₂ x₁], have x₂A : x₂ ∈ A, { apply not_imp_self.mp, assume x₂nA : x₂ ∉ A, rw [if_pos xA, if_neg x₂nA] at hxeq, rw [A_def, sb_set, mem_Union] at xA, have x₂eq : x₂ = g (f x₁), { rw [hxeq, sb_right_inv f g x₂nA] }, rcases xA with ⟨n, hn⟩, rw [A_def, sb_set, mem_Union], use n + 1, simp [sb_aux], exact ⟨x₁, hn, x₂eq.symm⟩ }, rw [if_pos xA, if_pos x₂A] at hxeq, exact hf hxeq }, push_neg at xA, rw [if_neg xA.1, if_neg xA.2] at hxeq, rw [←sb_right_inv f g xA.1, hxeq, sb_right_inv f g xA.2] end theorem sb_surjective (hf: injective f) (hg : injective g) : surjective (sb_fun f g) := begin set A := sb_set f g with A_def, set h := sb_fun f g with h_def, intro y, by_cases gyA : g y ∈ A, { rw [A_def, sb_set, mem_Union] at gyA, rcases gyA with ⟨n, hn⟩, cases n with n, { simp [sb_aux] at hn, contradiction }, simp [sb_aux] at hn, rcases hn with ⟨x, xmem, hx⟩, use x, have : x ∈ A, { rw [A_def, sb_set, mem_Union], exact ⟨n, xmem⟩ }, simp only [h_def, sb_fun, if_pos this], exact hg hx }, use g y, simp only [h_def, sb_fun, if_neg gyA], apply left_inverse_inv_fun hg end end
-
-
-
@@ -1,126 +0,0 @@import data.nat.gcd import data.real.irrational #print nat.coprime example (m n : nat) (h : m.coprime n) : m.gcd n = 1 := h example (m n : nat) (h : m.coprime n) : m.gcd n = 1 := by { rw nat.coprime at h, exact h } example : nat.coprime 12 7 := by norm_num example : nat.gcd 12 8 = 4 := by norm_num #check @nat.prime_def_lt example (p : ℕ) (prime_p : nat.prime p) : 2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1 := by rwa nat.prime_def_lt at prime_p #check nat.prime.eq_one_or_self_of_dvd example (p : ℕ) (prime_p : nat.prime p) : ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p := prime_p.eq_one_or_self_of_dvd example : nat.prime 17 := by norm_num -- commonly used example : nat.prime 2 := nat.prime_two example : nat.prime 3 := nat.prime_three #check @nat.prime.dvd_mul #check nat.prime.dvd_mul nat.prime_two #check nat.prime_two.dvd_mul lemma even_of_even_sqr {m : ℕ} (h : 2 ∣ m^2) : 2 ∣ m := begin rw [pow_two, nat.prime_two.dvd_mul] at h, cases h; assumption end example {m : ℕ} (h : 2 ∣ m^2) : 2 ∣ m := nat.prime.dvd_of_dvd_pow nat.prime_two h example (a b c : nat) (h : a * b = a * c) (h' : a ≠ 0) : b = c := begin -- library_search suggests the following: exact (mul_right_inj' h').mp h end example {m n : ℕ} (coprime_mn : m.coprime n) : m^2 ≠ 2 * n^2 := begin intro sqr_eq, have : 2 ∣ m, sorry, obtain ⟨k, meq⟩ := dvd_iff_exists_eq_mul_left.mp this, have : 2 * (2 * k^2) = 2 * n^2, { rw [←sqr_eq, meq], ring }, have : 2 * k^2 = n^2, sorry, have : 2 ∣ n, sorry, have : 2 ∣ m.gcd n, sorry, have : 2 ∣ 1, sorry, norm_num at this end example {m n p : ℕ} (coprime_mn : m.coprime n) (prime_p : p.prime) : m^2 ≠ p * n^2 := sorry #check nat.factors #check nat.prime_of_mem_factors #check nat.prod_factors #check nat.factors_unique theorem factorization_mul' {m n : ℕ} (mnez : m ≠ 0) (nnez : n ≠ 0) (p : ℕ) : (m * n).factorization p = m.factorization p + n.factorization p := by { rw nat.factorization_mul mnez nnez, refl } theorem factorization_pow' (n k p : ℕ) : (n^k).factorization p = k * n.factorization p := by { rw nat.factorization_pow, refl } theorem nat.prime.factorization' {p : ℕ} (prime_p : p.prime) : p.factorization p = 1 := by { rw prime_p.factorization, simp } example {m n p : ℕ} (nnz : n ≠ 0) (prime_p : p.prime) : m^2 ≠ p * n^2 := begin intro sqr_eq, have nsqr_nez : n^2 ≠ 0, by simpa, have eq1 : nat.factorization (m^2) p = 2 * m.factorization p, sorry, have eq2 : (p * n^2).factorization p = 2 * n.factorization p + 1, sorry, have : (2 * m.factorization p) % 2 = (2 * n.factorization p + 1) % 2, { rw [←eq1, sqr_eq, eq2] }, rw [add_comm, nat.add_mul_mod_self_left, nat.mul_mod_right] at this, norm_num at this end example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m^k = r * n^k) {p : ℕ} (prime_p : p.prime) : k ∣ r.factorization p := begin cases r with r, { simp }, have npow_nz : n^k ≠ 0 := λ npowz, nnz (pow_eq_zero npowz), have eq1 : (m^k).factorization p = k * m.factorization p, sorry, have eq2 : (r.succ * n^k).factorization p = k * n.factorization p + r.succ.factorization p, sorry, have : r.succ.factorization p = k * m.factorization p - k * n.factorization p, { rw [←eq1, pow_eq, eq2, add_comm, nat.add_sub_cancel] }, rw this, sorry end #check multiplicity #check @irrational_nrt_of_n_not_dvd_multiplicity #check irrational_sqrt_two
-
-
-
@@ -1,151 +0,0 @@import data.nat.prime import algebra.big_operators import tactic example (n : nat) : n.succ ≠ nat.zero := nat.succ_ne_zero n example (m n : nat) (h : m.succ = n.succ) : m = n := nat.succ.inj h def fac : ℕ → ℕ | 0 := 1 | (n + 1) := (n + 1) * fac n example : fac 0 = 1 := rfl example : fac 0 = 1 := by rw fac example : fac 0 = 1 := by simp [fac] example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := rfl example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := by rw fac example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := by simp [fac] theorem fac_pos (n : ℕ) : 0 < fac n := begin induction n with n ih, { rw fac, exact zero_lt_one }, rw fac, exact mul_pos n.succ_pos ih, end theorem dvd_fac {i n : ℕ} (ipos : 0 < i) (ile : i ≤ n) : i ∣ fac n := begin induction n with n ih, { exact absurd ipos (not_lt_of_ge ile) }, rw fac, cases nat.of_le_succ ile with h h, { apply dvd_mul_of_dvd_right (ih h) }, rw h, apply dvd_mul_right end theorem pow_two_le_fac (n : ℕ) : 2^(n-1) ≤ fac n := begin cases n with n, { simp [fac] }, sorry end section variables {α : Type*} (s : finset ℕ) (f : ℕ → ℕ) (n : ℕ) #check finset.sum s f #check finset.prod s f open_locale big_operators open finset example : s.sum f = ∑ x in s, f x := rfl example : s.prod f = ∏ x in s, f x := rfl example : (range n).sum f = ∑ x in range n, f x := rfl example : (range n).prod f = ∏ x in range n, f x := rfl example (f : ℕ → ℕ) : ∑ x in range 0, f x = 0 := finset.sum_range_zero f example (f : ℕ → ℕ) (n : ℕ): ∑ x in range n.succ, f x = (∑ x in range n, f x) + f n := finset.sum_range_succ f n example (f : ℕ → ℕ) : ∏ x in range 0, f x = 1 := finset.prod_range_zero f example (f : ℕ → ℕ) (n : ℕ): ∏ x in range n.succ, f x = (∏ x in range n, f x) * f n := finset.prod_range_succ f n example (n : ℕ) : fac n = ∏ i in range n, (i + 1) := begin induction n with n ih, { simp [fac] }, simp [fac, ih, prod_range_succ, mul_comm] end example (a b c d e f : ℕ) : a * ((b * c) * f * (d * e)) = d * (a * f * e) * (c * b) := by simp [mul_assoc, mul_comm, mul_left_comm] theorem sum_id (n : ℕ) : ∑ i in range (n + 1), i = n * (n + 1) / 2 := begin symmetry, apply nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2), induction n with n ih, { simp }, rw [finset.sum_range_succ, mul_add 2, ←ih, nat.succ_eq_add_one], ring end theorem sum_sqr (n : ℕ) : ∑ i in range (n + 1), i^2 = n * (n + 1) * (2 *n + 1) / 6 := sorry end inductive my_nat | zero : my_nat | succ : my_nat → my_nat namespace my_nat def add : my_nat → my_nat → my_nat | x zero := x | x (succ y) := succ (add x y) def mul : my_nat → my_nat → my_nat | x zero := zero | x (succ y) := add (mul x y) x theorem zero_add (n : my_nat) : add zero n = n := begin induction n with n ih, { refl }, rw [add, ih] end theorem succ_add (m n : my_nat) : add (succ m) n = succ (add m n) := begin induction n with n ih, { refl }, rw [add, ih], refl end theorem add_comm (m n : my_nat) : add m n = add n m := begin induction n with n ih, { rw zero_add, refl }, rw [add, succ_add, ih] end theorem add_assoc (m n k : my_nat) : add (add m n) k = add m (add n k) := sorry theorem mul_add (m n k : my_nat) : mul m (add n k) = add (mul m n) (mul m k) := sorry theorem zero_mul (n : my_nat) : mul zero n = zero := sorry theorem succ_mul (m n : my_nat) : mul (succ m) n = add (mul m n) n := sorry theorem mul_comm (m n : my_nat) : mul m n = mul n m := sorry end my_nat
-
-
-
@@ -1,254 +0,0 @@import data.nat.prime import algebra.big_operators import tactic open_locale big_operators theorem two_le {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := begin cases m, contradiction, cases m, contradiction, repeat { apply nat.succ_le_succ }, apply zero_le end example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := begin by_contradiction h, push_neg at h, interval_cases m; contradiction end example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := begin by_contradiction h, push_neg at h, revert m h h0 h1, dec_trivial end example {m : ℕ} (h : m < 2) : m = 0 ∨ m = 1 := by dec_trivial! example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by omega theorem exists_prime_factor {n : nat} (h : 2 ≤ n) : ∃ p : nat, p.prime ∧ p ∣ n := begin by_cases np : n.prime, { use [n, np, dvd_rfl] }, induction n using nat.strong_induction_on with n ih, dsimp at ih, rw nat.prime_def_lt at np, push_neg at np, rcases np h with ⟨m, mltn, mdvdn, mne1⟩, have : m ≠ 0, { intro mz, rw [mz, zero_dvd_iff] at mdvdn, linarith }, have mgt2 : 2 ≤ m := two_le this mne1, by_cases mp : m.prime, { use [m, mp, mdvdn] }, rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩, use [p, pp, pdvd.trans mdvdn] end theorem primes_infinite : ∀ n, ∃ p > n, nat.prime p := begin intro n, have : 2 ≤ nat.factorial (n + 1) + 1, sorry, rcases exists_prime_factor this with ⟨p, pp, pdvd⟩, refine ⟨p, _, pp⟩, show p > n, by_contradiction ple, push_neg at ple, have : p ∣ nat.factorial (n + 1), sorry, have : p ∣ 1, sorry, show false, sorry end open finset section variables {α : Type*} [decidable_eq α] (r s t : finset α) example : r ∩ (s ∪ t) ⊆ (r ∩ s) ∪ (r ∩ t) := begin rw subset_iff, intro x, rw [mem_inter, mem_union, mem_union, mem_inter, mem_inter], tauto end example : r ∩ (s ∪ t) ⊆ (r ∩ s) ∪ (r ∩ t) := by { simp [subset_iff], intro x, tauto } example : (r ∩ s) ∪ (r ∩ t) ⊆ r ∩ (s ∪ t) := by { simp [subset_iff], intro x, tauto } example : (r ∩ s) ∪ (r ∩ t) = r ∩ (s ∪ t) := by { ext x, simp, tauto } end section variables {α : Type*} [decidable_eq α] (r s t : finset α) example : (r ∪ s) ∩ (r ∪ t) = r ∪ (s ∩ t) := sorry example : (r \ s \ t) = r \ (s ∪ t) := sorry end example (s : finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ (∏ i in s, i) := finset.dvd_prod_of_mem _ h theorem nat.prime.eq_of_dvd_of_prime {p q : ℕ} (prime_p : nat.prime p) (prime_q : nat.prime q) (h : p ∣ q) : p = q := sorry theorem mem_of_dvd_prod_primes {s : finset ℕ} {p : ℕ} (prime_p : p.prime) : (∀ n ∈ s, nat.prime n) → (p ∣ ∏ n in s, n) → p ∈ s := begin intros h₀ h₁, induction s using finset.induction_on with a s ans ih, { simp at h₁, linarith [prime_p.two_le] }, simp [finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁, rw mem_insert, sorry end example (s : finset ℕ) (x : ℕ) : x ∈ s.filter nat.prime ↔ x ∈ s ∧ x.prime := mem_filter theorem primes_infinite' : ∀ (s : finset nat), ∃ p, nat.prime p ∧ p ∉ s := begin intro s, by_contradiction h, push_neg at h, set s' := s.filter nat.prime with s'_def, have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.prime, { intro n, simp [s'_def], apply h }, have : 2 ≤ (∏ i in s', i) + 1, sorry, rcases exists_prime_factor this with ⟨p, pp, pdvd⟩, have : p ∣ (∏ i in s', i), sorry, have : p ∣ 1, { convert nat.dvd_sub' pdvd this, simp }, show false, sorry end theorem bounded_of_ex_finset (Q : ℕ → Prop): (∃ s : finset ℕ, ∀ k, Q k → k ∈ s) → ∃ n, ∀ k, Q k → k < n := begin rintros ⟨s, hs⟩, use s.sup id + 1, intros k Qk, apply nat.lt_succ_of_le, show id k ≤ s.sup id, apply le_sup (hs k Qk) end theorem ex_finset_of_bounded (Q : ℕ → Prop) [decidable_pred Q] : (∃ n, ∀ k, Q k → k ≤ n) → (∃ s : finset ℕ, ∀ k, Q k ↔ k ∈ s) := begin rintros ⟨n, hn⟩, use (range (n + 1)).filter Q, intro k, simp [nat.lt_succ_iff], exact hn k end example : 27 % 4 = 3 := by norm_num example (n : ℕ) : (4 * n + 3) % 4 = 3 := by { rw [add_comm, nat.add_mul_mod_self_left], norm_num } theorem mod_4_eq_3_or_mod_4_eq_3 {m n : ℕ} (h : m * n % 4 = 3) : m % 4 = 3 ∨ n % 4 = 3 := begin revert h, rw [nat.mul_mod], have : m % 4 < 4 := nat.mod_lt m (by norm_num), interval_cases m % 4 with hm; simp [hm], have : n % 4 < 4 := nat.mod_lt n (by norm_num), interval_cases n % 4 with hn; simp [hn]; norm_num end theorem two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n := by apply two_le; { intro neq, rw neq at h, norm_num at h } theorem aux {m n : ℕ} (h₀ : m ∣ n) (h₁ : 2 ≤ m) (h₂ : m < n) : (n / m) ∣ n ∧ n / m < n := sorry theorem exists_prime_factor_mod_4_eq_3 {n : nat} (h : n % 4 = 3) : ∃ p : nat, p.prime ∧ p ∣ n ∧ p % 4 = 3 := begin by_cases np : n.prime, { use [n, np, dvd_rfl, h] }, induction n using nat.strong_induction_on with n ih, dsimp at ih, rw nat.prime_def_lt at np, push_neg at np, rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩, have mge2 : 2 ≤ m, { apply two_le _ mne1, intro mz, rw [mz, zero_dvd_iff] at mdvdn, linarith }, have neq : m * (n / m) = n := nat.mul_div_cancel' mdvdn, have : m % 4 = 3 ∨ (n / m) % 4 = 3, { apply mod_4_eq_3_or_mod_4_eq_3, rw [neq, h] }, cases this with h1 h1, { sorry }, sorry end example (m n : ℕ) (s : finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s := by rwa mem_erase at h example (m n : ℕ) (s : finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s := by { simp at h, assumption } theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, nat.prime p ∧ p % 4 = 3 := begin by_contradiction h, push_neg at h, cases h with n hn, have : ∃ s : finset nat, ∀ p : ℕ, p.prime ∧ p % 4 = 3 ↔ p ∈ s, { apply ex_finset_of_bounded, use n, contrapose! hn, rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩, exact ⟨p, pltn, pp, p4⟩ }, cases this with s hs, have h₀ : 2 ≤ 4 * (∏ i in erase s 3, i) + 3, sorry, have h₁ : (4 * (∏ i in erase s 3, i) + 3) % 4 = 3, sorry, rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩, have ps : p ∈ s, sorry, have pne3 : p ≠ 3, sorry, have : p ∣ 4 * (∏ i in erase s 3, i), sorry, have : p ∣ 3, sorry, have : p = 3, sorry, contradiction end
-
-
-
@@ -1,107 +0,0 @@import data.nat.gcd import data.real.irrational lemma even_of_even_sqr {m : ℕ} (h : 2 ∣ m^2) : 2 ∣ m := begin rw [pow_two, nat.prime_two.dvd_mul] at h, cases h; assumption end example {m n : ℕ} (coprime_mn : m.coprime n) : m^2 ≠ 2 * n^2 := begin intro sqr_eq, have : 2 ∣ m, { apply even_of_even_sqr, rw sqr_eq, apply dvd_mul_right }, obtain ⟨k, meq⟩ := dvd_iff_exists_eq_mul_left.mp this, have : 2 * (2 * k^2) = 2 * n^2, { rw [←sqr_eq, meq], ring }, have : 2 * k^2 = n^2, from (mul_right_inj' (by norm_num)).mp this, have : 2 ∣ n, { apply even_of_even_sqr, rw ←this, apply dvd_mul_right }, have : 2 ∣ m.gcd n, by apply nat.dvd_gcd; assumption, have : 2 ∣ 1, { convert this, symmetry, exact coprime_mn }, norm_num at this end example {m n p : ℕ} (coprime_mn : m.coprime n) (prime_p : p.prime) : m^2 ≠ p * n^2 := begin intro sqr_eq, have : p ∣ m, { apply prime_p.dvd_of_dvd_pow, rw sqr_eq, apply dvd_mul_right }, obtain ⟨k, meq⟩ := dvd_iff_exists_eq_mul_left.mp this, have : p * (p * k^2) = p * n^2, { rw [←sqr_eq, meq], ring }, have : p * k^2 = n^2, { apply (mul_right_inj' _).mp this, exact prime_p.ne_zero }, have : p ∣ n, { apply prime_p.dvd_of_dvd_pow, rw ←this, apply dvd_mul_right }, have : p ∣ nat.gcd m n, { apply nat.dvd_gcd; assumption }, have : p ∣ 1, { convert this, symmetry, exact coprime_mn }, have : 2 ≤ 1, { apply prime_p.two_le.trans, exact nat.le_of_dvd zero_lt_one this }, norm_num at this end theorem factorization_mul' {m n : ℕ} (mnez : m ≠ 0) (nnez : n ≠ 0) (p : ℕ) : (m * n).factorization p = m.factorization p + n.factorization p := by { rw nat.factorization_mul mnez nnez, refl } theorem factorization_pow' (n k p : ℕ) : (n^k).factorization p = k * n.factorization p := by { rw nat.factorization_pow, refl } theorem nat.prime.factorization' {p : ℕ} (prime_p : p.prime) : p.factorization p = 1 := by { rw prime_p.factorization, simp } example {m n p : ℕ} (nnz : n ≠ 0) (prime_p : p.prime) : m^2 ≠ p * n^2 := begin intro sqr_eq, have nsqr_nez : n^2 ≠ 0, by simpa, have eq1 : nat.factorization (m^2) p = 2 * m.factorization p, by { rw factorization_pow' }, have eq2 : (p * n^2).factorization p = 2 * n.factorization p + 1, { rw [factorization_mul' prime_p.ne_zero nsqr_nez, prime_p.factorization', factorization_pow', add_comm] }, have : (2 * m.factorization p) % 2 = (2 * n.factorization p + 1) % 2, { rw [←eq1, sqr_eq, eq2] }, rw [add_comm, nat.add_mul_mod_self_left, nat.mul_mod_right] at this, norm_num at this end example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m^k = r * n^k) {p : ℕ} (prime_p : p.prime) : k ∣ r.factorization p := begin cases r with r, { simp }, have npow_nz : n^k ≠ 0 := λ npowz, nnz (pow_eq_zero npowz), have eq1 : (m^k).factorization p = k * m.factorization p, by rw factorization_pow', have eq2 : (r.succ * n^k).factorization p = k * n.factorization p + r.succ.factorization p, { rw [factorization_mul' r.succ_ne_zero npow_nz, factorization_pow', add_comm] }, have : r.succ.factorization p = k * m.factorization p - k * n.factorization p, { rw [←eq1, pow_eq, eq2, add_comm, nat.add_sub_cancel] }, rw this, apply nat.dvd_sub'; apply nat.dvd_mul_right end
-
-
-
@@ -1,114 +0,0 @@import data.nat.prime import algebra.big_operators import tactic def fac : ℕ → ℕ | 0 := 1 | (n + 1) := (n + 1) * fac n theorem pow_two_le_fac (n : ℕ) : 2^(n-1) ≤ fac n := begin cases n with n, { simp [fac] }, induction n with n ih, { simp [fac] }, simp at *, rw [pow_succ, fac], apply nat.mul_le_mul _ ih, repeat { apply nat.succ_le_succ }, apply zero_le end section variables {α : Type*} (s : finset ℕ) (f : ℕ → ℕ) (n : ℕ) open_locale big_operators open finset theorem sum_sqr (n : ℕ) : ∑ i in range (n + 1), i^2 = n * (n + 1) * (2 *n + 1) / 6 := begin symmetry, apply nat.div_eq_of_eq_mul_right (by norm_num : 0 < 6), induction n with n ih, { simp }, rw [finset.sum_range_succ, mul_add 6, ←ih, nat.succ_eq_add_one], ring end end inductive my_nat | zero : my_nat | succ : my_nat → my_nat namespace my_nat def add : my_nat → my_nat → my_nat | x zero := x | x (succ y) := succ (add x y) def mul : my_nat → my_nat → my_nat | x zero := zero | x (succ y) := add (mul x y) x theorem zero_add (n : my_nat) : add zero n = n := begin induction n with n ih, { refl }, rw [add, ih] end theorem succ_add (m n : my_nat) : add (succ m) n = succ (add m n) := begin induction n with n ih, { refl }, rw [add, ih], refl end theorem add_comm (m n : my_nat) : add m n = add n m := begin induction n with n ih, { rw zero_add, refl }, rw [add, succ_add, ih] end theorem add_assoc (m n k : my_nat) : add (add m n) k = add m (add n k) := begin induction k with k ih, { refl }, rw [add, ih], refl end theorem mul_add (m n k : my_nat) : mul m (add n k) = add (mul m n) (mul m k) := begin induction k with k ih, { refl }, rw [add, mul, mul, ih, add_assoc] end theorem zero_mul (n : my_nat) : mul zero n = zero := begin induction n with n ih, { refl }, rw [mul, ih], refl end theorem succ_mul (m n : my_nat) : mul (succ m) n = add (mul m n) n := begin induction n with n ih, { refl }, rw [mul, mul, ih, add_assoc, add_assoc, add_comm n, succ_add], refl end theorem mul_comm (m n : my_nat) : mul m n = mul n m := begin induction n with n ih, { rw [zero_mul], refl }, rw [mul, ih, succ_mul] end end my_nat
-
-
-
@@ -1,246 +0,0 @@import data.nat.prime import algebra.big_operators import tactic open_locale big_operators theorem two_le {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := begin cases m, contradiction, cases m, contradiction, repeat { apply nat.succ_le_succ }, apply zero_le end theorem exists_prime_factor {n : nat} (h : 2 ≤ n) : ∃ p : nat, p.prime ∧ p ∣ n := begin by_cases np : n.prime, { use [n, np, dvd_rfl] }, induction n using nat.strong_induction_on with n ih, dsimp at ih, rw nat.prime_def_lt at np, push_neg at np, rcases np h with ⟨m, mltn, mdvdn, mne1⟩, have : m ≠ 0, { intro mz, rw [mz, zero_dvd_iff] at mdvdn, linarith }, have mgt2 : 2 ≤ m := two_le this mne1, by_cases mp : m.prime, { use [m, mp, mdvdn] }, rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩, use [p, pp, pdvd.trans mdvdn] end theorem primes_infinite : ∀ n, ∃ p > n, nat.prime p := begin intro n, have : 2 ≤ nat.factorial (n + 1) + 1, { apply nat.succ_le_succ, exact nat.succ_le_of_lt (nat.factorial_pos _) }, rcases exists_prime_factor this with ⟨p, pp, pdvd⟩, refine ⟨p, _, pp⟩, show p > n, by_contradiction ple, push_neg at ple, have : p ∣ nat.factorial (n + 1), { apply nat.dvd_factorial, apply pp.pos, linarith }, have : p ∣ 1, { convert nat.dvd_sub' pdvd this, simp }, show false, have := nat.le_of_dvd zero_lt_one this, linarith [pp.two_le] end open finset section variables {α : Type*} [decidable_eq α] (r s t : finset α) example : (r ∪ s) ∩ (r ∪ t) = r ∪ (s ∩ t) := begin ext x, rw [mem_inter, mem_union, mem_union, mem_union, mem_inter], tauto end example : (r ∪ s) ∩ (r ∪ t) = r ∪ (s ∩ t) := by { ext x, simp, tauto } example : (r \ s \ t) = r \ (s ∪ t) := begin ext x, rw [mem_sdiff, mem_sdiff, mem_sdiff, mem_union], tauto end example : (r \ s \ t) = r \ (s ∪ t) := by { ext x, simp, tauto } end theorem nat.prime.eq_of_dvd_of_prime {p q : ℕ} (prime_p : nat.prime p) (prime_q : nat.prime q) (h : p ∣ q) : p = q := begin cases prime_q.eq_one_or_self_of_dvd _ h, { linarith [prime_p.two_le] }, assumption end theorem mem_of_dvd_prod_primes {s : finset ℕ} {p : ℕ} (prime_p : p.prime) : (∀ n ∈ s, nat.prime n) → (p ∣ ∏ n in s, n) → p ∈ s := begin intros h₀ h₁, induction s using finset.induction_on with a s ans ih, { simp at h₁, linarith [prime_p.two_le] }, simp [finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁, rw mem_insert, cases h₁ with h₁ h₁, { left, exact prime_p.eq_of_dvd_of_prime h₀.1 h₁ }, right, exact ih h₀.2 h₁ end theorem primes_infinite' : ∀ (s : finset nat), ∃ p, nat.prime p ∧ p ∉ s := begin intro s, by_contradiction h, push_neg at h, set s' := s.filter nat.prime with s'_def, have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.prime, { intro n, simp [s'_def], apply h }, have : 2 ≤ (∏ i in s', i) + 1, { apply nat.succ_le_succ, apply nat.succ_le_of_lt, apply finset.prod_pos, intros n ns', apply (mem_s'.mp ns').pos }, rcases exists_prime_factor this with ⟨p, pp, pdvd⟩, have : p ∣ (∏ i in s', i), { apply dvd_prod_of_mem, rw mem_s', apply pp }, have : p ∣ 1, { convert nat.dvd_sub' pdvd this, simp }, show false, have := nat.le_of_dvd zero_lt_one this, linarith [pp.two_le] end theorem bounded_of_ex_finset (Q : ℕ → Prop): (∃ s : finset ℕ, ∀ k, Q k → k ∈ s) → ∃ n, ∀ k, Q k → k < n := begin rintros ⟨s, hs⟩, use s.sup id + 1, intros k Qk, apply nat.lt_succ_of_le, show id k ≤ s.sup id, apply le_sup (hs k Qk) end theorem ex_finset_of_bounded (Q : ℕ → Prop) [decidable_pred Q] : (∃ n, ∀ k, Q k → k ≤ n) → (∃ s : finset ℕ, ∀ k, Q k ↔ k ∈ s) := begin rintros ⟨n, hn⟩, use (range (n + 1)).filter Q, intro k, simp [nat.lt_succ_iff], exact hn k end theorem mod_4_eq_3_or_mod_4_eq_3 {m n : ℕ} (h : m * n % 4 = 3) : m % 4 = 3 ∨ n % 4 = 3 := begin revert h, rw [nat.mul_mod], have : m % 4 < 4 := nat.mod_lt m (by norm_num), interval_cases m % 4 with hm; simp [hm], have : n % 4 < 4 := nat.mod_lt n (by norm_num), interval_cases n % 4 with hn; simp [hn]; norm_num end theorem two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n := by apply two_le; { intro neq, rw neq at h, norm_num at h } theorem aux {m n : ℕ} (h₀ : m ∣ n) (h₁ : 2 ≤ m) (h₂ : m < n) : (n / m) ∣ n ∧ n / m < n := begin split, { exact nat.div_dvd_of_dvd h₀ }, exact nat.div_lt_self (lt_of_le_of_lt (zero_le _) h₂) h₁ end theorem exists_prime_factor_mod_4_eq_3 {n : nat} (h : n % 4 = 3) : ∃ p : nat, p.prime ∧ p ∣ n ∧ p % 4 = 3 := begin by_cases np : n.prime, { use [n, np, dvd_rfl, h] }, induction n using nat.strong_induction_on with n ih, dsimp at ih, rw nat.prime_def_lt at np, push_neg at np, rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩, have mge2 : 2 ≤ m, { apply two_le _ mne1, intro mz, rw [mz, zero_dvd_iff] at mdvdn, linarith }, have neq : m * (n / m) = n := nat.mul_div_cancel' mdvdn, have : m % 4 = 3 ∨ (n / m) % 4 = 3, { apply mod_4_eq_3_or_mod_4_eq_3, rw [neq, h] }, cases this with h1 h1, { by_cases mp : m.prime, { use [m, mp, mdvdn, h1] }, rcases ih m mltn h1 mp with ⟨p, pp, pdvd, p4eq⟩, use [p, pp, pdvd.trans mdvdn, p4eq] }, obtain ⟨nmdvdn, nmltn⟩ := aux mdvdn mge2 mltn, by_cases nmp : (n / m).prime, { use [n / m, nmp, nmdvdn, h1] }, rcases ih (n / m) nmltn h1 nmp with ⟨p, pp, pdvd, p4eq⟩, use [p, pp, pdvd.trans nmdvdn, p4eq] end theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, nat.prime p ∧ p % 4 = 3 := begin by_contradiction h, push_neg at h, cases h with n hn, have : ∃ s : finset nat, ∀ p : ℕ, p.prime ∧ p % 4 = 3 ↔ p ∈ s, { apply ex_finset_of_bounded, use n, contrapose! hn, rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩, exact ⟨p, pltn, pp, p4⟩ }, cases this with s hs, have h₀ : 2 ≤ 4 * (∏ i in erase s 3, i) + 3, { apply le_add_left, norm_num }, have h₁ : (4 * (∏ i in erase s 3, i) + 3) % 4 = 3, { rw [add_comm, nat.add_mul_mod_self_left], norm_num }, rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩, have ps : p ∈ s, { rw ←hs p, exact ⟨pp, p4eq⟩ }, have pne3 : p ≠ 3, { intro peq, rw [peq, ←nat.dvd_add_iff_left (dvd_refl 3)] at pdvd, rw nat.prime_three.dvd_mul at pdvd, norm_num at pdvd, have : 3 ∈ s.erase 3, { apply mem_of_dvd_prod_primes nat.prime_three _ pdvd, intro n, simp [← hs n], tauto }, simp at this, exact this }, have : p ∣ 4 * (∏ i in erase s 3, i), { apply dvd_trans _ (dvd_mul_left _ _), apply dvd_prod_of_mem, simp, split; assumption }, have : p ∣ 3, { convert nat.dvd_sub' pdvd this, simp }, have : p = 3, { apply pp.eq_of_dvd_of_prime nat.prime_three this }, contradiction end
-
-
-
@@ -1,228 +0,0 @@import algebra.big_operators.ring import data.real.basic @[ext] structure point := (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 := begin ext, repeat { assumption } end def my_point1 : point := { x := 2, y := -1, z := 4 } def my_point2 := { point . x := 2, y := -1, z := 4 } def my_point3 : point := ⟨2, -1, 4⟩ def my_point4 := point.mk 2 (-1) 4 structure point' := 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 := { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z } #check add my_point1 my_point2 #check my_point1.add my_point2 end point #check point.add my_point1 my_point2 #check my_point1.add my_point2 namespace point protected theorem add_comm (a b : point) : add a b = add b a := begin rw [add, add], ext; dsimp, repeat { apply add_comm } end 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 add_alt : point → point → point | (point.mk x₁ y₁ z₁) (point.mk x₂ y₂ z₂) := ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩ def add_alt' : point → point → point | ⟨x₁, y₁, z₁⟩ ⟨x₂, y₂, z₂⟩ := ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩ theorem add_alt_x (a b : point) : (a.add_alt b).x = a.x + b.x := by { cases a, cases b, refl } theorem add_alt_comm (a b : point) : add_alt a b = add_alt b a := begin rcases a with ⟨xa, ya, za⟩, rcases b with ⟨xb, yb, zb⟩, rw [add_alt, add_alt], ext; dsimp, apply add_comm, repeat { apply add_comm }, end example (a b : point) : add_alt a b = add_alt b a := begin rcases a with ⟨xa, ya, za⟩, rcases b with ⟨xb, yb, zb⟩, simp [add_alt, add_comm] end example : ∀ a b : point, add_alt a b = add_alt b a := begin rintros ⟨xa, ya, za⟩ ⟨xb, yb, zb⟩, simp [add_alt, add_comm] end example : ∀ a b : point, add a b = add b a := λ ⟨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) := 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) := sorry end point structure standard_two_simplex := (x : ℝ) (y : ℝ) (z : ℝ) (x_nonneg : 0 ≤ x) (y_nonneg : 0 ≤ y) (z_nonneg : 0 ≤ z) (sum_eq : x + y + z = 1) namespace standard_two_simplex def swap_xy (a : standard_two_simplex) : standard_two_simplex := { 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 theory def midpoint (a b : standard_two_simplex) : standard_two_simplex := { 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 weighted_average (lambda : real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : standard_two_simplex) : standard_two_simplex := sorry end standard_two_simplex open_locale big_operators structure standard_simplex (n : ℕ) := (v : fin n → ℝ) (nonneg : ∀ i : fin n, 0 ≤ v i) (sum_eq_one : ∑ i, v i = 1) namespace standard_simplex def midpoint (n : ℕ) (a b : standard_simplex n) : standard_simplex n := { v := λ i, (a.v i + b.v i) / 2, nonneg := begin intro i, apply div_nonneg, { linarith [a.nonneg i, b.nonneg i] }, norm_num end, sum_eq_one := begin simp [div_eq_mul_inv, ←finset.sum_mul, finset.sum_add_distrib, a.sum_eq_one, b.sum_eq_one], field_simp end } end standard_simplex structure is_linear (f : ℝ → ℝ) := (is_additive : ∀ x y, f (x + y) = f x + f y) (preserves_mul : ∀ x c, f (c * x) = c * f x) section variables (f : ℝ → ℝ) (linf : is_linear f) #check linf.is_additive #check linf.preserves_mul end def point'' := ℝ × ℝ × ℝ def is_linear' (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 standard_two_simplex' := { p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 } def standard_simplex' (n : ℕ) := { v : fin n → ℝ // (∀ i : fin n, 0 ≤ v i) ∧ (∑ i, v i = 1) } def std_simplex := Σ n : ℕ, standard_simplex n section variable s : std_simplex #check s.fst #check s.snd #check s.1 #check s.2 end
-
-
-
@@ -1,154 +0,0 @@import data.real.basic structure group₁ (α : Type*) := (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 x one = x) (mul_left_inv : ∀ x : α, mul (inv x) x = one) structure Group₁ := (α : Type*) (str : group₁ α) section variables (α β γ : Type*) variables (f : α ≃ β) (g : β ≃ γ) #check equiv α β #check (f.to_fun : α → β) #check (f.inv_fun : β → α) #check (f.right_inv: ∀ x : β, f (f.inv_fun x) = x) #check (f.left_inv: ∀ x : α, f.inv_fun (f x) = x) #check (equiv.refl α : α ≃ α) #check (f.symm : β ≃ α) #check (f.trans g : α ≃ γ) example (x : α) : (f.trans g).to_fun x = g.to_fun (f.to_fun 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 perm_group {α : Type*} : group₁ (equiv.perm α) := { 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 add_group₁ (α : Type*) := (add : α → α → α) -- fill in the rest @[ext] structure point := (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 b : point) : point := sorry def zero : point := sorry def add_group_point : add_group point := sorry end point section variables {α : 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*) := (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 x one = x) (mul_left_inv : ∀ x : α, mul (inv x) x = one) instance {α : Type*} : group₂ (equiv.perm α) := { 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 my_square {α : Type*} [group₂ α] (x : α) := group₂.mul x x #check @my_square section variables {β : Type*} (f g : equiv.perm β) example : group₂.mul f g = g.trans f := rfl example : my_square f = f.trans f := rfl end instance : inhabited point := { default := ⟨0, 0, 0⟩ } #check (default : point) example : ([] : list point).head = default := rfl instance : has_add point := { add := point.add } section variables x y : point #check x + y example : x + y = point.add x y := rfl end instance has_mul_group₂ {α : Type*} [group₂ α] : has_mul α := ⟨group₂.mul⟩ instance has_one_group₂ {α : Type*} [group₂ α] : has_one α := ⟨group₂.one⟩ instance has_inv_group₂ {α : Type*} [group₂ α] : has_inv α := ⟨group₂.inv⟩ section variables {α : Type*} (f g : equiv.perm α) #check f * 1 * g⁻¹ def foo: f * 1 * g⁻¹ = g.symm.trans ((equiv.refl α).trans f) := rfl end class add_group₂ (α : Type*) := (add : α → α → α) -- fill in the rest
-
-
-
@@ -1,194 +0,0 @@import data.int.basic import ring_theory.principal_ideal_domain import tactic @[ext] structure gaussint := (re : ℤ) (im : ℤ) namespace gaussint instance : has_zero gaussint := ⟨⟨0, 0⟩⟩ instance : has_one gaussint := ⟨⟨1, 0⟩⟩ instance : has_add gaussint := ⟨λ x y, ⟨x.re + y.re, x.im + y.im⟩⟩ instance : has_neg gaussint := ⟨λ x, ⟨-x.re, -x.im⟩⟩ instance : has_mul gaussint := ⟨λ 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 : comm_ring gaussint := { 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 } } 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.div_add_mod a b example (a b : ℤ) : b ≠ 0 → 0 ≤ a % b := int.mod_nonneg a example (a b : ℤ) : b ≠ 0 → a % b < abs b := int.mod_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 := begin rw [div', mod'], linarith [int.div_add_mod (a + b / 2) b], end theorem abs_mod'_le (a b : ℤ) (h : 0 < b): abs (mod' a b) ≤ b / 2 := begin rw [mod', abs_le], split, { linarith [int.mod_nonneg (a + b / 2) h.ne'] }, have := int.mod_lt_of_pos (a + b / 2) h, have := int.div_add_mod b 2, have := int.mod_lt_of_pos b zero_lt_two, linarith end 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*} [linear_ordered_ring α] (x y : α) : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := sorry namespace gaussint def norm (x : gaussint) := x.re^2 + x.im^2 @[simp] theorem norm_nonneg (x : gaussint) : 0 ≤ norm x := sorry theorem norm_eq_zero (x : gaussint) : norm x = 0 ↔ x = 0 := sorry theorem norm_pos (x : gaussint) : 0 < norm x ↔ x ≠ 0 := sorry theorem norm_mul (x y : gaussint) : norm (x * y) = norm x * norm y := 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 : has_div gaussint := ⟨λ x y, ⟨int.div' (x * conj y).re (norm y), int.div' (x * conj y).im (norm y)⟩⟩ instance : has_mod gaussint := ⟨λ 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 lemma norm_mod_lt (x : gaussint) {y : gaussint} (hy : y ≠ 0) : (x % y).norm < y.norm := begin 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)⟩, { rw [mod_def, sub_mul, int.mod'_eq, int.mod'_eq, sub_eq_add_neg, norm, div_def], ext; simp; ring }, have : norm (x % y) * norm y ≤ (norm y / 2) * norm y, { conv { to_lhs, rw [←norm_conj y, ←norm_mul, this, norm] }, simp, transitivity 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.div_mul_le, norm_num }, apply int.div_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.div_lt_of_lt_mul, { norm_num }, linarith end lemma coe_nat_abs_norm (x : gaussint) : (x.norm.nat_abs : ℤ) = x.norm := int.nat_abs_of_nonneg (norm_nonneg _) lemma nat_abs_norm_mod_lt (x y : gaussint) (hy : y ≠ 0) : (x % y).norm.nat_abs < y.norm.nat_abs := begin apply int.coe_nat_lt.1, simp, exact int.nat_abs_lt_nat_abs_of_nonneg_of_lt (norm_nonneg _) (norm_mod_lt x hy) end lemma not_norm_mul_left_lt_norm (x : gaussint) {y : gaussint} (hy : y ≠ 0) : ¬ (norm (x * y)).nat_abs < (norm x).nat_abs := begin apply not_lt_of_ge, rw [norm_mul, int.nat_abs_mul], apply le_mul_of_one_le_right (nat.zero_le _), apply int.coe_nat_le.1, rw [coe_nat_abs_norm], exact int.add_one_le_of_lt ((norm_pos _).mpr hy) end instance : euclidean_domain gaussint := { quotient := (/), remainder := (%), quotient_mul_add_remainder_eq := λ x y, by {rw [mod_def, add_comm, sub_add_cancel] }, quotient_zero := λ x, by { simp [div_def, norm, int.div'], refl }, r := measure (int.nat_abs ∘ norm), r_well_founded := measure_wf (int.nat_abs ∘ norm), remainder_lt := nat_abs_norm_mod_lt, mul_left_not_lt := not_norm_mul_left_lt_norm, .. gaussint.comm_ring } example (x : gaussint) : irreducible x ↔ prime x := principal_ideal_ring.irreducible_iff_prime end gaussint
-
-
-
@@ -1,101 +0,0 @@import algebra.big_operators.ring import data.real.basic @[ext] structure point := (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 standard_two_simplex := (x : ℝ) (y : ℝ) (z : ℝ) (x_nonneg : 0 ≤ x) (y_nonneg : 0 ≤ y) (z_nonneg : 0 ≤ z) (sum_eq : x + y + z = 1) namespace standard_two_simplex noncomputable theory def weighted_average (lambda : real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : standard_two_simplex) : standard_two_simplex := { 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 := begin transitivity (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 standard_two_simplex open_locale big_operators structure standard_simplex (n : ℕ) := (v : fin n → ℝ) (nonneg : ∀ i : fin n, 0 ≤ v i) (sum_eq_one : ∑ i, v i = 1) namespace standard_simplex def midpoint (n : ℕ) (a b : standard_simplex n) : standard_simplex n := { v := λ i, (a.v i + b.v i) / 2, nonneg := begin intro i, apply div_nonneg, { linarith [a.nonneg i, b.nonneg i] }, norm_num end, sum_eq_one := begin simp [div_eq_mul_inv, ←finset.sum_mul, finset.sum_add_distrib, a.sum_eq_one, b.sum_eq_one], field_simp end } end standard_simplex namespace standard_simplex def weighted_average {n : ℕ} (lambda : real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : standard_simplex n) : standard_simplex n := { 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 := begin transitivity 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 } end standard_simplex
-
-
-
@@ -1,65 +0,0 @@import data.real.basic structure add_group₁ (α : Type*) := (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 := (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 add_group_point : add_group₁ point := { 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], intro, ext; refl }, zero_add := by { simp [point.add, point.zero], intro, ext; refl }, add_left_neg := by { simp [point.add, point.neg, point.zero] } } end point class add_group₂ (α : Type*) := (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 has_add_add_group₂ {α : Type*} [add_group₂ α] : has_add α := ⟨add_group₂.add⟩ instance has_zero_add_group₂ {α : Type*} [add_group₂ α] : has_zero α := ⟨add_group₂.zero⟩ instance has_neg_add_group₂ {α : Type*} [add_group₂ α] : has_neg α := ⟨add_group₂.neg⟩ instance : add_group₂ point := { 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], intro, ext; refl }, zero_add := by { simp [point.add, point.zero], intro, ext; refl }, add_left_neg := by { simp [point.add, point.neg, point.zero] } } section variables (x y : point) #check x + -y + 0 end
-
-
-
@@ -1,206 +0,0 @@import data.int.basic import ring_theory.principal_ideal_domain import tactic @[ext] structure gaussint := (re : ℤ) (im : ℤ) namespace gaussint instance : has_zero gaussint := ⟨⟨0, 0⟩⟩ instance : has_one gaussint := ⟨⟨1, 0⟩⟩ instance : has_add gaussint := ⟨λ x y, ⟨x.re + y.re, x.im + y.im⟩⟩ instance : has_neg gaussint := ⟨λ x, ⟨-x.re, -x.im⟩⟩ instance : has_mul gaussint := ⟨λ 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 : comm_ring gaussint := { 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 } } 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 := begin rw [div', mod'], linarith [int.div_add_mod (a + b / 2) b], end theorem abs_mod'_le (a b : ℤ) (h : 0 < b): abs (mod' a b) ≤ b / 2 := begin rw [mod', abs_le], split, { linarith [int.mod_nonneg (a + b / 2) h.ne'] }, have := int.mod_lt_of_pos (a + b / 2) h, have := int.div_add_mod b 2, have := int.mod_lt_of_pos b zero_lt_two, linarith end 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*} [linear_ordered_ring α] {x y : α} (h : x^2 + y^2 = 0) : x = 0 := begin have h' : x^2 = 0, { apply le_antisymm _ (sq_nonneg x), rw ←h, apply le_add_of_nonneg_right (sq_nonneg y) }, exact pow_eq_zero h' end theorem sq_add_sq_eq_zero {α : Type*} [linear_ordered_ring α] (x y : α) : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := begin split, { intro h, split, { exact aux h }, rw add_comm at h, exact aux h }, rintros ⟨rfl, rfl⟩, norm_num end 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], refl } 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 : has_div gaussint := ⟨λ x y, ⟨int.div' (x * conj y).re (norm y), int.div' (x * conj y).im (norm y)⟩⟩ instance : has_mod gaussint := ⟨λ 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 lemma norm_mod_lt (x : gaussint) {y : gaussint} (hy : y ≠ 0) : (x % y).norm < y.norm := begin 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)⟩, { rw [mod_def, sub_mul, int.mod'_eq, int.mod'_eq, sub_eq_add_neg, norm, div_def], ext; simp; ring }, have : norm (x % y) * norm y ≤ (norm y / 2) * norm y, { conv { to_lhs, rw [←norm_conj y, ←norm_mul, this, norm] }, simp, transitivity 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.div_mul_le, norm_num }, apply int.div_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.div_lt_of_lt_mul, { norm_num }, linarith end lemma coe_nat_abs_norm (x : gaussint) : (x.norm.nat_abs : ℤ) = x.norm := int.nat_abs_of_nonneg (norm_nonneg _) lemma nat_abs_norm_mod_lt (x y : gaussint) (hy : y ≠ 0) : (x % y).norm.nat_abs < y.norm.nat_abs := begin apply int.coe_nat_lt.1, simp, exact int.nat_abs_lt_nat_abs_of_nonneg_of_lt (norm_nonneg _) (norm_mod_lt x hy) end lemma not_norm_mul_left_lt_norm (x : gaussint) {y : gaussint} (hy : y ≠ 0) : ¬ (norm (x * y)).nat_abs < (norm x).nat_abs := begin apply not_lt_of_ge, rw [norm_mul, int.nat_abs_mul], apply le_mul_of_one_le_right (nat.zero_le _), apply int.coe_nat_le.1, rw [coe_nat_abs_norm], exact int.add_one_le_of_lt ((norm_pos _).mpr hy) end instance : euclidean_domain gaussint := { quotient := (/), remainder := (%), quotient_mul_add_remainder_eq := λ x y, by {rw [mod_def, add_comm, sub_add_cancel] }, quotient_zero := λ x, by { simp [div_def, norm, int.div'], refl }, r := measure (int.nat_abs ∘ norm), r_well_founded := measure_wf (int.nat_abs ∘ norm), remainder_lt := nat_abs_norm_mod_lt, mul_left_not_lt := not_norm_mul_left_lt_norm, .. gaussint.comm_ring } example (x : gaussint) : irreducible x ↔ prime x := principal_ideal_ring.irreducible_iff_prime end gaussint
-
-
src/07_Topology/01_Filters.lean (deleted)
-
@@ -1,106 +0,0 @@import topology.instances.real open set filter open_locale topological_space filter def principal {α : Type*} (s : set α) : filter α := { 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 variables (f : ℝ → ℝ) (x₀ y₀ : ℝ) #check comap (coe : ℚ → ℝ) (𝓝 x₀) #check tendsto (f ∘ coe) (comap (coe : ℚ → ℝ) (𝓝 x₀)) (𝓝 y₀) section variables {α β γ : 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 at_top (𝓝 (x₀, y₀)) ↔ tendsto (prod.fst ∘ f) at_top (𝓝 x₀) ∧ tendsto (prod.snd ∘ f) at_top (𝓝 y₀) := sorry example (x₀ : ℝ) : has_basis (𝓝 x₀) (λ ε : ℝ, 0 < ε) (λ ε, Ioo (x₀ - ε) (x₀ + ε)) := nhds_basis_Ioo_pos x₀ example (u : ℕ → ℝ) (x₀ : ℝ) : tendsto u at_top (𝓝 x₀) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ∈ Ioo (x₀ - ε) (x₀ + ε) := begin have : at_top.has_basis (λ n : ℕ, true) Ici := at_top_basis, rw this.tendsto_iff (nhds_basis_Ioo_pos x₀), simp end example (P Q : ℕ → Prop) (hP : ∀ᶠ n in at_top, P n) (hQ : ∀ᶠ n in at_top, Q n) : ∀ᶠ n in at_top, P n ∧ Q n := hP.and hQ example (u v : ℕ → ℝ) (h : ∀ᶠ n in at_top, u n = v n) (x₀ : ℝ) : tendsto u at_top (𝓝 x₀) ↔ tendsto v at_top (𝓝 x₀) := tendsto_congr' h example (u v : ℕ → ℝ) (h : u =ᶠ[at_top] v) (x₀ : ℝ) : tendsto u at_top (𝓝 x₀) ↔ tendsto v at_top (𝓝 x₀) := tendsto_congr' h #check @eventually_of_forall #check @eventually.mono #check @eventually.and example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in at_top, P n) (hQ : ∀ᶠ n in at_top, Q n) (hR : ∀ᶠ n in at_top, P n ∧ Q n → R n) : ∀ᶠ n in at_top, R n := begin apply (hP.and (hQ.and hR)).mono, rintros n ⟨h, h', h''⟩, exact h'' ⟨h, h'⟩ end example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in at_top, P n) (hQ : ∀ᶠ n in at_top, Q n) (hR : ∀ᶠ n in at_top, P n ∧ Q n → R n) : ∀ᶠ n in at_top, R n := begin filter_upwards [hP, hQ, hR], intros n h h' h'', exact h'' ⟨h, h'⟩ end #check mem_closure_iff_cluster_pt #check le_principal_iff #check ne_bot_of_le example (u : ℕ → ℝ) (M : set ℝ) (x : ℝ) (hux : tendsto u at_top (𝓝 x)) (huM : ∀ᶠ n in at_top, u n ∈ M) : x ∈ closure M := sorry
-
-
src/07_Topology/02_Metric_Spaces.lean (deleted)
-
@@ -1,252 +0,0 @@import topology.instances.real import analysis.normed_space.banach_steinhaus open set filter open_locale topological_space filter variables {X : Type*} [metric_space 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 emetric_space #check pseudo_metric_space #check pseudo_emetric_space example {u : ℕ → X} {a : X} : tendsto u at_top (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := metric.tendsto_at_top example {X Y : Type*} [metric_space X] [metric_space 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*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ p : X × X, dist (f p.1) (f p.2)) := by continuity example {X Y : Type*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ 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*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ p : X × X, dist (f p.1) (f p.2)) := begin apply continuous.dist, exact hf.comp continuous_fst, exact hf.comp continuous_snd end example {X Y : Type*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ p : X × X, dist (f p.1) (f p.2)) := (hf.comp continuous_fst).dist (hf.comp continuous_snd) example {X Y : Type*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ p : X × X, dist (f p.1) (f p.2)) := hf.fst'.dist hf.snd' example {f : ℝ → X} (hf : continuous f) : continuous (λ x : ℝ, f (x^2 + x)) := sorry example {X Y : Type*} [metric_space X] [metric_space Y] (f : X → Y) (a : X) : continuous_at f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x}, dist x a < δ → dist (f x) (f a) < ε := metric.continuous_at_iff variables r : ℝ example : metric.ball a r = {b | dist b a < r} := rfl example : metric.closed_ball 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.closed_ball a r := metric.mem_closed_ball_self hr example (s : set X) : is_open s ↔ ∀ x ∈ s, ∃ ε > 0, metric.ball x ε ⊆ s := metric.is_open_iff example {s : set X} : is_closed s ↔ is_open sᶜ := is_open_compl_iff.symm example {s : set X} (hs : is_closed s) {u : ℕ → X} (hu : tendsto u at_top (𝓝 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 at_top (𝓝 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.closed_ball x ε ⊆ s := metric.nhds_basis_closed_ball.mem_iff example : is_compact (set.Icc 0 1 : set ℝ) := is_compact_Icc example {s : set X} (hs : is_compact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, strict_mono φ ∧ tendsto (u ∘ φ) at_top (𝓝 a) := hs.tendsto_subseq hu example {s : set X} (hs : is_compact s) (hs' : s.nonempty) {f : X → ℝ} (hfs : continuous_on f s) : ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y := hs.exists_forall_le hs' hfs example {s : set X} (hs : is_compact s) (hs' : s.nonempty) {f : X → ℝ} (hfs : continuous_on f s) : ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x := hs.exists_forall_ge hs' hfs example {s : set X} (hs : is_compact s) : is_closed s := hs.is_closed example {X : Type*} [metric_space X] [compact_space X] : is_compact (univ : set X) := compact_univ #check is_compact.is_closed example {X : Type*} [metric_space X] {Y : Type*} [metric_space Y] {f : X → Y} : uniform_continuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := metric.uniform_continuous_iff example {X : Type*} [metric_space X] [compact_space X] {Y : Type*} [metric_space Y] {f : X → Y} (hf : continuous f) : uniform_continuous f := sorry example (u : ℕ → X) : cauchy_seq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := metric.cauchy_seq_iff example (u : ℕ → X) : cauchy_seq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := metric.cauchy_seq_iff' example [complete_space X] (u : ℕ → X) (hu : cauchy_seq u) : ∃ x, tendsto u at_top (𝓝 x) := cauchy_seq_tendsto_of_complete hu open_locale big_operators open finset lemma cauchy_seq_of_le_geometric_two' {u : ℕ → X} (hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : cauchy_seq u := begin rw metric.cauchy_seq_iff', intros ε ε_pos, obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε, { sorry }, use N, intros 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 end open metric example [complete_space X] (f : ℕ → set X) (ho : ∀ n, is_open (f n)) (hd : ∀ n, dense (f n)) : dense (⋂n, f n) := begin let B : ℕ → ℝ := λ 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, { sorry }, choose! center radius Hpos HB Hball using this, intros x, rw mem_closure_iff_nhds_basis nhds_basis_closed_ball, intros ε ε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 × ℝ) := λn, nat.rec_on n (prod.mk x (min ε (B 0))) (λn p, prod.mk (center n p.1 p.2) (radius n p.1 p.2)), let c : ℕ → X := λ n, (F n).1, let r : ℕ → ℝ := λ n, (F n).2, have rpos : ∀ n, 0 < r n, { sorry }, have rB : ∀n, r n ≤ B n, { sorry }, have incl : ∀n, closed_ball (c (n+1)) (r (n+1)) ⊆ (closed_ball (c n) (r n)) ∩ (f n), { sorry }, have cdist : ∀ n, dist (c n) (c (n+1)) ≤ B n, { sorry }, have : cauchy_seq c, from cauchy_seq_of_le_geometric_two' cdist, -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`. rcases cauchy_seq_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), { sorry }, have yball : ∀n, y ∈ closed_ball (c n) (r n), { sorry }, sorry end
-
-
-
@@ -1,200 +0,0 @@import topology.instances.real import analysis.normed_space.banach_steinhaus open set filter open_locale topological_space filter section variables {X : Type*} [topological_space X] example : is_open (univ : set X) := is_open_univ example : is_open (∅ : set X) := is_open_empty example {ι : Type*} {s : ι → set X} (hs : ∀ i, is_open $ s i) : is_open (⋃ i, s i) := is_open_Union hs example {ι : Type*} [fintype ι] {s : ι → set X} (hs : ∀ i, is_open $ s i) : is_open (⋂ i, s i) := is_open_Inter hs variables {Y : Type*} [topological_space Y] example {f : X → Y} : continuous f ↔ ∀ s, is_open s → is_open (f ⁻¹' s) := continuous_def example {f : X → Y} {x : X} : continuous_at f x ↔ map f (𝓝 x) ≤ 𝓝 (f x) := iff.rfl example {f : X → Y} {x : X} : continuous_at f x ↔ ∀ U ∈ 𝓝 (f x), ∀ᶠ x in 𝓝 x, f x ∈ U := iff.rfl example {x : X} {s : set X} : s ∈ 𝓝 x ↔ ∃ t ⊆ s, is_open 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 topological_space.mk_of_nhds #check topological_space.nhds_mk_of_nhds. 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. variables {X Y : Type*} example (f : X → Y) : topological_space X → topological_space Y := topological_space.coinduced f example (f : X → Y) : topological_space Y → topological_space X := topological_space.induced f example (f : X → Y) (T_X : topological_space X) (T_Y : topological_space Y) : topological_space.coinduced f T_X ≤ T_Y ↔ T_X ≤ topological_space.induced f T_Y := coinduced_le_iff_le_induced #check coinduced_compose #check induced_compose. example {T T' : topological_space X} : T ≤ T' ↔ ∀ s, T'.is_open s → T.is_open s := iff.rfl example (T_X : topological_space X) (T_Y : topological_space Y) (f : X → Y) : continuous f ↔ topological_space.coinduced f T_X ≤ T_Y := continuous_iff_coinduced_le example {Z : Type*} (f : X → Y) (T_X : topological_space X) (T_Z : topological_space Z) (g : Y → Z) : @continuous Y Z (topological_space.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, topological_space $ X i) : (Pi.topological_space : topological_space (Π i, X i)) = ⨅ i, topological_space.induced (λ x, x i) (T_X i) := rfl example [topological_space X] [t2_space X] {u : ℕ → X} {a b : X} (ha : tendsto u at_top (𝓝 a)) (hb : tendsto u at_top (𝓝 b)) : a = b := tendsto_nhds_unique ha hb example [topological_space X] [regular_space X] (a : X) : (𝓝 a).has_basis (λ (s : set X), s ∈ 𝓝 a ∧ is_closed s) id := closed_nhds_basis a example [topological_space X] {x : X} : (𝓝 x).has_basis (λ t : set X, t ∈ 𝓝 x ∧ is_open t) id := nhds_basis_opens' x lemma aux {X Y A : Type*} [topological_space 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, is_open V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := sorry example [topological_space X] [topological_space Y] [regular_space Y] {A : set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : continuous f) (hf : ∀ x : X, ∃ c : Y, tendsto f (comap coe $ 𝓝 x) $ 𝓝 c) : ∃ φ : X → Y, continuous φ ∧ ∀ a : A, φ a = f a := sorry example [topological_space X] [topological_space.first_countable_topology X] {s : set X} {a : X} : a ∈ closure s ↔ ∃ (u : ℕ → X), (∀ n, u n ∈ s) ∧ tendsto u at_top (𝓝 a) := mem_closure_iff_seq_limit variables [topological_space X] example {F : filter X} {x : X} : cluster_pt x F ↔ ne_bot (𝓝 x ⊓ F) := iff.rfl example {s : set X} : is_compact s ↔ ∀ (F : filter X) [ne_bot F], F ≤ 𝓟 s → ∃ a ∈ s, cluster_pt a F := iff.rfl example [topological_space.first_countable_topology X] {s : set X} {u : ℕ → X} (hs : is_compact s) (hu : ∀ n, u n ∈ s) : ∃ (a ∈ s) (φ : ℕ → ℕ), strict_mono φ ∧ tendsto (u ∘ φ) at_top (𝓝 a) := hs.tendsto_subseq hu variables [topological_space Y] example {x : X} {F : filter X} {G : filter Y} (H : cluster_pt x F) {f : X → Y} (hfx : continuous_at f x) (hf : tendsto f F G) : cluster_pt (f x) G := cluster_pt.map H hfx hf example [topological_space Y] {f : X → Y} (hf : continuous f) {s : set X} (hs : is_compact s) : is_compact (f '' s) := begin intros F F_ne F_le, have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F, { sorry }, haveI Hne : (𝓟 s ⊓ comap f F).ne_bot, { sorry }, have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s, from inf_le_left, sorry end example {ι : Type*} {s : set X} (hs : is_compact s) (U : ι → set X) (hUo : ∀ i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ t : finset ι, s ⊆ ⋃ i ∈ t, U i := hs.elim_finite_subcover U hUo hsU example [compact_space X] : is_compact (univ : set X) := compact_univ
-
-
-
@@ -1,75 +0,0 @@import topology.instances.real open set filter open_locale topological_space filter -- 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 := λ U V hU hUV, subset.trans hU hUV, inter_sets := λ U V hU hV, subset_inter hU hV } example : filter ℕ := { sets := {s | ∃ a, ∀ b, a ≤ b → b ∈ s}, univ_sets := begin use 42, finish, end, sets_of_superset := begin rintros U V ⟨N, hN⟩ hUV, use N, tauto, end, inter_sets := begin rintros U V ⟨N, hN⟩ ⟨N', hN'⟩, use max N N', intros b hb, rw max_le_iff at hb, split ; tauto, end } 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 := begin intros V hV, rw preimage_comp, apply hf, apply hg, exact hV end example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) : tendsto f at_top (𝓝 (x₀, y₀)) ↔ tendsto (prod.fst ∘ f) at_top (𝓝 x₀) ∧ tendsto (prod.snd ∘ f) at_top (𝓝 y₀) := calc tendsto f at_top (𝓝 (x₀, y₀)) ↔ map f at_top ≤ 𝓝 (x₀, y₀) : iff.rfl ... ↔ map f at_top ≤ 𝓝 x₀ ×ᶠ 𝓝 y₀ : by rw nhds_prod_eq ... ↔ map f at_top ≤ (comap prod.fst (𝓝 x₀) ⊓ comap prod.snd (𝓝 y₀)) : iff.rfl ... ↔ map f at_top ≤ comap prod.fst (𝓝 x₀) ∧ map f at_top ≤ (comap prod.snd (𝓝 y₀)) : le_inf_iff ... ↔ map prod.fst (map f at_top) ≤ 𝓝 x₀ ∧ map prod.snd (map f at_top) ≤ 𝓝 y₀ : by rw [← map_le_iff_le_comap, ← map_le_iff_le_comap] ... ↔ map (prod.fst ∘ f) at_top ≤ 𝓝 x₀ ∧ map (prod.snd ∘ f) at_top ≤ 𝓝 y₀ : by rw [map_map, map_map] -- an alternative solution example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) : tendsto f at_top (𝓝 (x₀, y₀)) ↔ tendsto (prod.fst ∘ f) at_top (𝓝 x₀) ∧ tendsto (prod.snd ∘ f) at_top (𝓝 y₀) := begin 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] end example (u : ℕ → ℝ) (M : set ℝ) (x : ℝ) (hux : tendsto u at_top (𝓝 x)) (huM : ∀ᶠ n in at_top, u n ∈ M) : x ∈ closure M := mem_closure_iff_cluster_pt.mpr (ne_bot_of_le $ le_inf hux $ le_principal_iff.mpr huM)
-
-
-
@@ -1,410 +0,0 @@import topology.instances.real import analysis.normed_space.banach_steinhaus open set filter open_locale topological_space filter variables {X : Type*} [metric_space 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 emetric_space #check pseudo_metric_space #check pseudo_emetric_space example {u : ℕ → X} {a : X} : tendsto u at_top (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := metric.tendsto_at_top example {X Y : Type*} [metric_space X] [metric_space 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*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ p : X × X, dist (f p.1) (f p.2)) := by continuity example {X Y : Type*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ 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*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ p : X × X, dist (f p.1) (f p.2)) := begin apply continuous.dist, exact hf.comp continuous_fst, exact hf.comp continuous_snd end example {X Y : Type*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ p : X × X, dist (f p.1) (f p.2)) := (hf.comp continuous_fst).dist (hf.comp continuous_snd) example {X Y : Type*} [metric_space X] [metric_space Y] {f : X → Y} (hf : continuous f) : continuous (λ p : X × X, dist (f p.1) (f p.2)) := hf.fst'.dist hf.snd' example {f : ℝ → X} (hf : continuous f) : continuous (λ x : ℝ, f (x^2 + x)) := sorry example {f : ℝ → X} (hf : continuous f) : continuous (λ x : ℝ, f (x^2 + x)) := hf.comp $ (continuous_pow 2).add continuous_id example {X Y : Type*} [metric_space X] [metric_space Y] (f : X → Y) (a : X) : continuous_at f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x}, dist x a < δ → dist (f x) (f a) < ε := metric.continuous_at_iff variables r : ℝ example : metric.ball a r = {b | dist b a < r} := rfl example : metric.closed_ball 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.closed_ball a r := metric.mem_closed_ball_self hr example (s : set X) : is_open s ↔ ∀ x ∈ s, ∃ ε > 0, metric.ball x ε ⊆ s := metric.is_open_iff example {s : set X} : is_closed s ↔ is_open sᶜ := is_open_compl_iff.symm example {s : set X} (hs : is_closed s) {u : ℕ → X} (hu : tendsto u at_top (𝓝 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 at_top (𝓝 a)) {s : set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := sorry example {u : ℕ → X} (hu : tendsto u at_top (𝓝 a)) {s : set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := begin rw metric.tendsto_at_top at hu, rw metric.mem_closure_iff, intros ε ε_pos, rcases hu ε ε_pos with ⟨N, hN⟩, refine ⟨u N, hs _, _⟩, rw dist_comm, exact hN N le_rfl end 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.closed_ball x ε ⊆ s := metric.nhds_basis_closed_ball.mem_iff example : is_compact (set.Icc 0 1 : set ℝ) := is_compact_Icc example {s : set X} (hs : is_compact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, strict_mono φ ∧ tendsto (u ∘ φ) at_top (𝓝 a) := hs.tendsto_subseq hu example {s : set X} (hs : is_compact s) (hs' : s.nonempty) {f : X → ℝ} (hfs : continuous_on f s) : ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y := hs.exists_forall_le hs' hfs example {s : set X} (hs : is_compact s) (hs' : s.nonempty) {f : X → ℝ} (hfs : continuous_on f s) : ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x := hs.exists_forall_ge hs' hfs example {s : set X} (hs : is_compact s) : is_closed s := hs.is_closed example {X : Type*} [metric_space X] [compact_space X] : is_compact (univ : set X) := compact_univ #check is_compact.is_closed example {X : Type*} [metric_space X] {Y : Type*} [metric_space Y] {f : X → Y} : uniform_continuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := metric.uniform_continuous_iff example {X : Type*} [metric_space X] [compact_space X] {Y : Type*} [metric_space Y] {f : X → Y} (hf : continuous f) : uniform_continuous f := sorry example {X : Type*} [metric_space X] [compact_space X] {Y : Type*} [metric_space Y] {f : X → Y} (hf : continuous f) : uniform_continuous f := begin rw metric.uniform_continuous_iff, intros ε ε_pos, let φ : X × X → ℝ := λ 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 : is_closed K := is_closed_le continuous_const φ_cont, have K_cpct : is_compact K := K_closed.is_compact, cases eq_empty_or_nonempty K with hK hK, { use [1, by norm_num], intros 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₁, split, { change _ < _, rw dist_pos, intro h, have : ε ≤ 0, by simpa [*] using xx_in, linarith }, { intros x x', contrapose!, intros hxx', exact H (x, x') hxx' } }, end example (u : ℕ → X) : cauchy_seq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := metric.cauchy_seq_iff example (u : ℕ → X) : cauchy_seq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := metric.cauchy_seq_iff' example [complete_space X] (u : ℕ → X) (hu : cauchy_seq u) : ∃ x, tendsto u at_top (𝓝 x) := cauchy_seq_tendsto_of_complete hu open_locale big_operators open finset lemma cauchy_seq_of_le_geometric_two' {u : ℕ → X} (hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : cauchy_seq u := begin rw metric.cauchy_seq_iff', intros ε ε_pos, obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε, { sorry }, use N, intros 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 end example {u : ℕ → X} (hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : cauchy_seq u := begin rw metric.cauchy_seq_iff', intros ε ε_pos, obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε, { have : tendsto (λ N : ℕ, (1 / 2 ^ N * 2 : ℝ)) at_top (𝓝 0), { rw ← zero_mul (2 : ℝ), apply tendsto.mul, simp_rw ← one_div_pow (2 : ℝ), apply tendsto_pow_at_top_nhds_0_of_lt_1 ; linarith, exact tendsto_const_nhds }, rcases (at_top_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, intros 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 (λ i, u (N+i)) k ... ≤ ∑ i in range k, (1/2 : ℝ) ^ (N+i) : sum_le_sum (λ 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 end open metric example [complete_space X] (f : ℕ → set X) (ho : ∀ n, is_open (f n)) (hd : ∀ n, dense (f n)) : dense (⋂n, f n) := begin let B : ℕ → ℝ := λ 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, { sorry }, choose! center radius Hpos HB Hball using this, intros x, rw mem_closure_iff_nhds_basis nhds_basis_closed_ball, intros ε ε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 × ℝ) := λn, nat.rec_on n (prod.mk x (min ε (B 0))) (λn p, prod.mk (center n p.1 p.2) (radius n p.1 p.2)), let c : ℕ → X := λ n, (F n).1, let r : ℕ → ℝ := λ n, (F n).2, have rpos : ∀ n, 0 < r n, { sorry }, have rB : ∀n, r n ≤ B n, { sorry }, have incl : ∀n, closed_ball (c (n+1)) (r (n+1)) ⊆ (closed_ball (c n) (r n)) ∩ (f n), { sorry }, have cdist : ∀ n, dist (c n) (c (n+1)) ≤ B n, { sorry }, have : cauchy_seq c, from cauchy_seq_of_le_geometric_two' cdist, -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`. rcases cauchy_seq_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), { sorry }, have yball : ∀n, y ∈ closed_ball (c n) (r n), { sorry }, sorry end example [complete_space X] (f : ℕ → set X) (ho : ∀ n, is_open (f n)) (hd : ∀ n, dense (f n)) : dense (⋂n, f n) := begin let B : ℕ → ℝ := λ n, (1/2)^n, have Bpos : ∀ n, 0 < B n, from λ 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, { intros 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 (is_open_iff_mem_nhds.1 (ho n) y ys), refine ⟨y, min (min (δ/2) r) (B (n+1)), _, _, λz hz, ⟨_, _⟩⟩, show 0 < min (min (δ / 2) r) (B (n+1)), from lt_min (lt_min (half_pos δpos) rpos) (Bpos (n+1)), show min (min (δ / 2) r) (B (n+1)) ≤ B (n+1), from min_le_right _ _, show z ∈ closed_ball x δ, from 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, from 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 λ x, (mem_closure_iff_nhds_basis nhds_basis_closed_ball).2 (λ ε ε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 × ℝ) := λn, nat.rec_on n (prod.mk x (min ε (B 0))) (λn p, prod.mk (center n p.1 p.2) (radius n p.1 p.2)), let c : ℕ → X := λ n, (F n).1, let r : ℕ → ℝ := λ n, (F n).2, have rpos : ∀ n, 0 < r n, { assume 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, { assume 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) := λ n, Hball n (c n) (r n) (rpos n), have cdist : ∀ n, dist (c n) (c (n+1)) ≤ B n, { assume 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 : cauchy_seq c, from cauchy_seq_of_le_geometric_two' cdist, -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`. rcases cauchy_seq_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), { assume n, refine nat.le_induction _ (λ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), { assume n, refine is_closed_ball.mem_of_tendsto ylim _, refine (filter.eventually_ge_at_top n).mono (λ m hm, _), exact I n m hm (mem_closed_ball_self (rpos _).le) }, split, { suffices : ∀ n, y ∈ f n, by rwa set.mem_Inter, 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 _ _, end
-
-
-
@@ -1,263 +0,0 @@import topology.instances.real import analysis.normed_space.banach_steinhaus open set filter open_locale topological_space filter section variables {X : Type*} [topological_space X] example : is_open (univ : set X) := is_open_univ example : is_open (∅ : set X) := is_open_empty example {ι : Type*} {s : ι → set X} (hs : ∀ i, is_open $ s i) : is_open (⋃ i, s i) := is_open_Union hs example {ι : Type*} [fintype ι] {s : ι → set X} (hs : ∀ i, is_open $ s i) : is_open (⋂ i, s i) := is_open_Inter hs variables {Y : Type*} [topological_space Y] example {f : X → Y} : continuous f ↔ ∀ s, is_open s → is_open (f ⁻¹' s) := continuous_def example {f : X → Y} {x : X} : continuous_at f x ↔ map f (𝓝 x) ≤ 𝓝 (f x) := iff.rfl example {f : X → Y} {x : X} : continuous_at f x ↔ ∀ U ∈ 𝓝 (f x), ∀ᶠ x in 𝓝 x, f x ∈ U := iff.rfl example {x : X} {s : set X} : s ∈ 𝓝 x ↔ ∃ t ⊆ s, is_open 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 topological_space.mk_of_nhds #check topological_space.nhds_mk_of_nhds. 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' := begin intros a s s_in, refine ⟨{y | s ∈ n y}, H a (λ x, x ∈ s) s_in, _, by tauto⟩, rintros y (hy : s ∈ n y), exact H₀ y hy end end -- BOTH. variables {X Y : Type*} example (f : X → Y) : topological_space X → topological_space Y := topological_space.coinduced f example (f : X → Y) : topological_space Y → topological_space X := topological_space.induced f example (f : X → Y) (T_X : topological_space X) (T_Y : topological_space Y) : topological_space.coinduced f T_X ≤ T_Y ↔ T_X ≤ topological_space.induced f T_Y := coinduced_le_iff_le_induced #check coinduced_compose #check induced_compose. example {T T' : topological_space X} : T ≤ T' ↔ ∀ s, T'.is_open s → T.is_open s := iff.rfl example (T_X : topological_space X) (T_Y : topological_space Y) (f : X → Y) : continuous f ↔ topological_space.coinduced f T_X ≤ T_Y := continuous_iff_coinduced_le example {Z : Type*} (f : X → Y) (T_X : topological_space X) (T_Z : topological_space Z) (g : Y → Z) : @continuous Y Z (topological_space.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, topological_space $ X i) : (Pi.topological_space : topological_space (Π i, X i)) = ⨅ i, topological_space.induced (λ x, x i) (T_X i) := rfl example [topological_space X] [t2_space X] {u : ℕ → X} {a b : X} (ha : tendsto u at_top (𝓝 a)) (hb : tendsto u at_top (𝓝 b)) : a = b := tendsto_nhds_unique ha hb example [topological_space X] [regular_space X] (a : X) : (𝓝 a).has_basis (λ (s : set X), s ∈ 𝓝 a ∧ is_closed s) id := closed_nhds_basis a example [topological_space X] {x : X} : (𝓝 x).has_basis (λ t : set X, t ∈ 𝓝 x ∧ is_open t) id := nhds_basis_opens' x lemma aux {X Y A : Type*} [topological_space 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, is_open V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := sorry example {X Y A : Type*} [topological_space 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, is_open V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := begin simpa [and_assoc] using ((nhds_basis_opens' x).comap c).tendsto_left_iff.mp h V' V'_in end example [topological_space X] [topological_space Y] [regular_space Y] {A : set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : continuous f) (hf : ∀ x : X, ∃ c : Y, tendsto f (comap coe $ 𝓝 x) $ 𝓝 c) : ∃ φ : X → Y, continuous φ ∧ ∀ a : A, φ a = f a := sorry example [topological_space X] [topological_space Y] [regular_space Y] {A : set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : continuous f) (hf : ∀ x : X, ∃ c : Y, tendsto f (comap coe $ 𝓝 x) $ 𝓝 c) : ∃ φ : X → Y, continuous φ ∧ ∀ a : A, φ a = f a := begin choose φ hφ using hf, use φ, split, { rw continuous_iff_continuous_at, intros x, suffices : ∀ V' ∈ 𝓝 (φ x), is_closed V' → φ ⁻¹' V' ∈ 𝓝 x, by simpa [continuous_at, (closed_nhds_basis _).tendsto_right_iff], intros V' V'_in V'_closed, obtain ⟨V, V_in, V_op, hV⟩ : ∃ V ∈ 𝓝 x, is_open V ∧ coe ⁻¹' V ⊆ f ⁻¹' V', { exact aux (hφ x) V'_in }, suffices : ∀ y ∈ V, φ y ∈ V', from mem_of_superset V_in this, intros y y_in, have hVx : V ∈ 𝓝 y := V_op.mem_nhds y_in, haveI : (comap (coe : A → X) (𝓝 y)).ne_bot := by simpa [mem_closure_iff_comap_ne_bot] using hA y, apply V'_closed.mem_of_tendsto (hφ y), exact mem_of_superset (preimage_mem_comap hVx) hV }, { intros a, have lim : tendsto f (𝓝 a) (𝓝 $ φ a), by simpa [nhds_induced] using hφ a, exact tendsto_nhds_unique lim f_cont.continuous_at }, end example [topological_space X] [topological_space.first_countable_topology X] {s : set X} {a : X} : a ∈ closure s ↔ ∃ (u : ℕ → X), (∀ n, u n ∈ s) ∧ tendsto u at_top (𝓝 a) := mem_closure_iff_seq_limit variables [topological_space X] example {F : filter X} {x : X} : cluster_pt x F ↔ ne_bot (𝓝 x ⊓ F) := iff.rfl example {s : set X} : is_compact s ↔ ∀ (F : filter X) [ne_bot F], F ≤ 𝓟 s → ∃ a ∈ s, cluster_pt a F := iff.rfl example [topological_space.first_countable_topology X] {s : set X} {u : ℕ → X} (hs : is_compact s) (hu : ∀ n, u n ∈ s) : ∃ (a ∈ s) (φ : ℕ → ℕ), strict_mono φ ∧ tendsto (u ∘ φ) at_top (𝓝 a) := hs.tendsto_subseq hu variables [topological_space Y] example {x : X} {F : filter X} {G : filter Y} (H : cluster_pt x F) {f : X → Y} (hfx : continuous_at f x) (hf : tendsto f F G) : cluster_pt (f x) G := cluster_pt.map H hfx hf example [topological_space Y] {f : X → Y} (hf : continuous f) {s : set X} (hs : is_compact s) : is_compact (f '' s) := begin intros F F_ne F_le, have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F, { sorry }, haveI Hne : (𝓟 s ⊓ comap f F).ne_bot, { sorry }, have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s, from inf_le_left, sorry end example [topological_space Y] {f : X → Y} (hf : continuous f) {s : set X} (hs : is_compact s) : is_compact (f '' s) := begin intros F F_ne F_le, have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F, { rw [filter.push_pull, map_principal] }, haveI Hne : (𝓟 s ⊓ comap f F).ne_bot, { apply ne_bot.of_map, rwa [map_eq, inf_of_le_right F_le] }, have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s, from 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.continuous_at, rw [tendsto, map_eq], exact inf_le_right end example {ι : Type*} {s : set X} (hs : is_compact s) (U : ι → set X) (hUo : ∀ i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ t : finset ι, s ⊆ ⋃ i ∈ t, U i := hs.elim_finite_subcover U hUo hsU example [compact_space X] : is_compact (univ : set X) := compact_univ
-
-
-
@@ -1,61 +0,0 @@import analysis.special_functions.trigonometric.deriv import analysis.calculus.mean_value open set filter open_locale topological_space filter classical real noncomputable theory open real /-- The sin function has derivative 1 at 0. -/ example : has_deriv_at sin 1 0 := by simpa using has_deriv_at_sin 0 example (x : ℝ) : differentiable_at ℝ sin x := (has_deriv_at_sin x).differentiable_at example {f : ℝ → ℝ} {x a : ℝ} (h : has_deriv_at f a x) : deriv f x = a := h.deriv example {f : ℝ → ℝ} {x : ℝ} (h : ¬ differentiable_at ℝ f x) : deriv f x = 0 := deriv_zero_of_not_differentiable_at h example {f g : ℝ → ℝ} {x : ℝ} (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) : deriv (f + g) x = deriv f x + deriv g x := deriv_add hf hg example {f : ℝ → ℝ} {a : ℝ} (h : is_local_min f a) : deriv f a = 0 := h.deriv_eq_zero example {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hfc : continuous_on f (Icc a b)) (hfI : f a = f b) : ∃ c ∈ Ioo a b, deriv f c = 0 := exists_deriv_eq_zero f hab hfc hfI example (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hf : continuous_on f (Icc a b)) (hf' : differentiable_on ℝ f (Ioo a b)) : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) := exists_deriv_eq_slope f hab hf hf' example : deriv (λ x : ℝ, x^5) 6 = 5 * 6^4 := by simp example (x₀ : ℝ) (h₀ : x₀ ≠ 0) : deriv (λ x : ℝ, 1 / x) x₀ = -(x₀^2)⁻¹ := by simp example : deriv sin π = -1 := by simp example (x₀ : ℝ) (h : x₀ ≠ 0) : deriv (λ x : ℝ, exp(x^2) / x^5) x₀ = (2 * x₀^2 - 5) * exp (x₀^2) / x₀^6 := begin have : x₀^5 ≠ 0, { exact pow_ne_zero 5 h, }, field_simp, ring, end example (y : ℝ) : has_deriv_at (λ x : ℝ, 2 * x + 5) 2 y := begin have := ((has_deriv_at_id y).const_mul 2).add_const 5, rwa [mul_one] at this, end example (y : ℝ) : deriv (λ x : ℝ, 2 * x + 5) y = 2 := by simp
-
-
-
@@ -1,193 +0,0 @@import analysis.normed_space.banach_steinhaus import analysis.normed_space.finite_dimension import analysis.calculus.inverse open set filter open_locale topological_space filter noncomputable theory section variables {E : Type*} [normed_group E] example (x : E) : 0 ≤ ∥x∥ := norm_nonneg x example {x : E} : ∥x∥ = 0 ↔ x = 0 := norm_eq_zero example (x y : E) : ∥x + y∥ ≤ ∥x∥ + ∥y∥ := norm_add_le x y example : metric_space E := by apply_instance example {X : Type*} [topological_space X] {f : X → E} (hf : continuous f) : continuous (λ x, ∥f x∥) := hf.norm variables [normed_space ℝ E] example (a : ℝ) (x : E) : ∥a • x∥ = |a| * ∥x∥ := norm_smul a x example [finite_dimensional ℝ E] : complete_space E := by apply_instance example (𝕜 : Type*) [nondiscrete_normed_field 𝕜] (x y : 𝕜) : ∥x * y∥ = ∥x∥ * ∥y∥ := norm_mul x y example (𝕜 : Type*) [nondiscrete_normed_field 𝕜] : ∃ x : 𝕜, 1 < ∥x∥ := normed_field.exists_one_lt_norm 𝕜 example (𝕜 : Type*) [nondiscrete_normed_field 𝕜] (E : Type*) [normed_group E] [normed_space 𝕜 E] [complete_space 𝕜] [finite_dimensional 𝕜 E] : complete_space E := finite_dimensional.complete 𝕜 E end section variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E] {F : Type*} [normed_group F] [normed_space 𝕜 F] example : E →L[𝕜] E := continuous_linear_map.id 𝕜 E example (f : E →L[𝕜] F) : E → F := f example (f : E →L[𝕜] F) : continuous f := f.cont example (f : E →L[𝕜] F) (x y : E) : f (x + y) = f x + f y := f.map_add x y example (f : E →L[𝕜] F) (a : 𝕜) (x : E) : f (a • x) = a • f x := f.map_smul a x variables (f : E →L[𝕜] F) example (x : E) : ∥f x∥ ≤ ∥f∥ * ∥x∥ := f.le_op_norm x example {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ x, ∥f x∥ ≤ M * ∥x∥) : ∥f∥ ≤ M := f.op_norm_le_bound hMp hM end section variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E] {F : Type*} [normed_group F] [normed_space 𝕜 F] open metric example {ι : Type*} [complete_space E] {g : ι → E →L[𝕜] F} (h : ∀ x, ∃ C, ∀ i, ∥g i x∥ ≤ C) : ∃ C', ∀ i, ∥g i∥ ≤ C' := begin /- sequence of subsets consisting of those `x : E` with norms `∥g i x∥` bounded by `n` -/ let e : ℕ → set E := λ n, ⋂ i : ι, { x : E | ∥g i x∥ ≤ n }, /- each of these sets is closed -/ have hc : ∀ n : ℕ, is_closed (e n), sorry, /- the union is the entire space; this is where we use `h` -/ have hU : (⋃ n : ℕ, e n) = univ, sorry, /- apply the Baire category theorem to conclude that for some `m : ℕ`, `e m` contains some `x` -/ obtain ⟨m, x, hx⟩ : ∃ m, ∃ x, x ∈ interior (e m) := sorry, obtain ⟨ε, ε_pos, hε⟩ : ∃ ε > 0, ball x ε ⊆ interior (e m) := sorry, obtain ⟨k, hk⟩ : ∃ k : 𝕜, 1 < ∥k∥ := sorry, /- show all elements in the ball have norm bounded by `m` after applying any `g i` -/ have real_norm_le : ∀ (z ∈ ball x ε) (i : ι), ∥g i z∥ ≤ m, sorry, have εk_pos : 0 < ε / ∥k∥ := sorry, refine ⟨(m + m : ℕ) / (ε / ∥k∥), λ i, continuous_linear_map.op_norm_le_of_shell ε_pos _ hk _⟩, sorry, sorry end end open asymptotics open_locale asymptotics example {α : Type*} {E : Type*} [normed_group E] {F : Type*} [normed_group F] (c : ℝ) (l : filter α) (f : α → E) (g : α → F) : is_O_with c l f g ↔ ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥ := is_O_with_iff example {α : Type*} {E : Type*} [normed_group E] {F : Type*} [normed_group F] (c : ℝ) (l : filter α) (f : α → E) (g : α → F) : f =O[l] g ↔ ∃ C, is_O_with C l f g := is_O_iff_is_O_with example {α : Type*} {E : Type*} [normed_group E] {F : Type*} [normed_group F] (c : ℝ) (l : filter α) (f : α → E) (g : α → F) : f =o[l] g ↔ ∀ C > 0, is_O_with C l f g := is_o_iff_forall_is_O_with example {α : Type*} {E : Type*} [normed_group E] (c : ℝ) (l : filter α) (f g : α → E) : f ~[l] g ↔ (f - g) =o[l] g := iff.rfl section variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E] {F : Type*} [normed_group F] [normed_space 𝕜 F] example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) : has_fderiv_at f f' x₀ ↔ (λ x, f x - f x₀ - f' (x - x₀)) =o[𝓝 x₀] (λ x, x - x₀) := iff.rfl example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) (hff' : has_fderiv_at f f' x₀) : fderiv 𝕜 f x₀ = f' := hff'.fderiv example (n : ℕ) (f : E → F) : E → (E [×n]→L[𝕜] F) := iterated_fderiv 𝕜 n f example (n : with_top ℕ) {f : E → F} : cont_diff 𝕜 n f ↔ (∀ (m : ℕ), (m : with_top ℕ) ≤ n → continuous (λ x, iterated_fderiv 𝕜 m f x)) ∧ (∀ (m : ℕ), (m : with_top ℕ) < n → differentiable 𝕜 (λ x, iterated_fderiv 𝕜 m f x)) := cont_diff_iff_continuous_differentiable example {𝕂 : Type*} [is_R_or_C 𝕂] {E : Type*} [normed_group E] [normed_space 𝕂 E] {F : Type*} [normed_group F] [normed_space 𝕂 F] {f : E → F} {x : E} {n : with_top ℕ} (hf : cont_diff_at 𝕂 n f x) (hn : 1 ≤ n) : has_strict_fderiv_at f (fderiv 𝕂 f x) x := hf.has_strict_fderiv_at hn section local_inverse variables [complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} example (hf : has_strict_fderiv_at f ↑f' a) : F → E := has_strict_fderiv_at.local_inverse f f' a hf example (hf : has_strict_fderiv_at f (f' : E →L[𝕜] F) a) : ∀ᶠ x in 𝓝 a, hf.local_inverse f f' a (f x) = x := hf.eventually_left_inverse example (hf : has_strict_fderiv_at f (f' : E →L[𝕜] F) a) : ∀ᶠ x in 𝓝 (f a), f (hf.local_inverse f f' a x) = x := hf.eventually_right_inverse example [complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f ↑f' a) : has_strict_fderiv_at (has_strict_fderiv_at.local_inverse f f' a hf) (f'.symm : F →L[𝕜] E) (f a) := has_strict_fderiv_at.to_local_inverse hf end local_inverse #check has_fderiv_within_at #check has_fderiv_at_filter end
-
-
-
@@ -1,8 +0,0 @@import analysis.special_functions.trigonometric.deriv import analysis.calculus.mean_value open set filter open_locale topological_space filter classical real noncomputable theory
-
-
src/08_Differential_Calculus/solutions/solutions_02_Differential_Calculus_in_Normed_Spaces.lean (deleted)
-
@@ -1,61 +0,0 @@import analysis.normed_space.banach_steinhaus import analysis.normed_space.finite_dimension import analysis.calculus.inverse open set filter open_locale topological_space filter noncomputable theory section variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E] {F : Type*} [normed_group F] [normed_space 𝕜 F] open metric example {ι : Type*} [complete_space E] {g : ι → E →L[𝕜] F} (h : ∀ x, ∃ C, ∀ i, ∥g i x∥ ≤ C) : ∃ C', ∀ i, ∥g i∥ ≤ C' := begin /- sequence of subsets consisting of those `x : E` with norms `∥g i x∥` bounded by `n` -/ let e : ℕ → set E := λ n, ⋂ i : ι, { x : E | ∥g i x∥ ≤ n }, /- each of these sets is closed -/ have hc : ∀ n : ℕ, is_closed (e n), from λ i, is_closed_Inter (λ i, is_closed_le (g i).cont.norm continuous_const), /- the union is the entire space; this is where we use `h` -/ have hU : (⋃ n : ℕ, e n) = univ, { refine eq_univ_of_forall (λ x, _), cases h x with C hC, obtain ⟨m, hm⟩ := exists_nat_ge C, exact ⟨e m, mem_range_self m, mem_Inter.mpr (λ i, le_trans (hC i) hm)⟩ }, /- apply the Baire category theorem to conclude that for some `m : ℕ`, `e m` contains some `x` -/ obtain ⟨m : ℕ, x : E, hx : x ∈ interior (e m)⟩ := nonempty_interior_of_Union_of_closed hc hU, obtain ⟨ε, ε_pos, hε : ball x ε ⊆ interior (e m)⟩ := is_open_iff.mp is_open_interior x hx, obtain ⟨k : 𝕜, hk : 1 < ∥k∥⟩ := normed_field.exists_one_lt_norm 𝕜, /- show all elements in the ball have norm bounded by `m` after applying any `g i` -/ have real_norm_le : ∀ (z ∈ ball x ε) (i : ι), ∥g i z∥ ≤ m, { intros z hz i, replace hz := mem_Inter.mp (interior_Inter_subset _ (hε hz)) i, apply interior_subset hz }, have εk_pos : 0 < ε / ∥k∥ := div_pos ε_pos (zero_lt_one.trans hk), refine ⟨(m + m : ℕ) / (ε / ∥k∥), λ i, continuous_linear_map.op_norm_le_of_shell ε_pos _ hk _⟩, { exact div_nonneg (nat.cast_nonneg _) εk_pos.le }, intros y le_y y_lt, calc ∥g i y∥ = ∥g i (y + x) - g i x∥ : by rw [(g i).map_add, add_sub_cancel] ... ≤ ∥g i (y + x)∥ + ∥g i x∥ : norm_sub_le _ _ ... ≤ m + m : add_le_add (real_norm_le (y + x) (by rwa [add_comm, add_mem_ball_iff_norm]) i) (real_norm_le x (mem_ball_self ε_pos) i) ... = (m + m : ℕ) : by norm_cast ... ≤ (m + m : ℕ) * (∥y∥ / (ε / ∥k∥)) : le_mul_of_one_le_right (nat.cast_nonneg _) ((one_le_div $ div_pos ε_pos (zero_lt_one.trans hk)).2 le_y) ... = (m + m : ℕ) / (ε / ∥k∥) * ∥y∥ : (mul_comm_div _ _ _).symm, end end
-
-
-
@@ -1,35 +0,0 @@import measure_theory.integral.interval_integral import analysis.special_functions.integrals import analysis.convolution open set filter open_locale topological_space filter noncomputable theory open measure_theory interval_integral open_locale interval -- this introduces the notation [a, b] example (a b : ℝ): ∫ x in a..b, x = (b ^ 2 - a ^ 2) / 2 := integral_id example {a b : ℝ} (h : (0:ℝ) ∉ [a, b]) : ∫ x in a..b, 1/x = real.log (b / a) := integral_one_div h example (f : ℝ → ℝ) (hf : continuous f) (a b : ℝ) : deriv (λ u, ∫ (x : ℝ) in a..u, f x) b = f b := (integral_has_strict_deriv_at_right (hf.interval_integrable _ _) (hf.strongly_measurable_at_filter _ _) hf.continuous_at).has_deriv_at.deriv example {f : ℝ → ℝ} {a b : ℝ} {f' : ℝ → ℝ} (h : ∀ x ∈ [a, b], has_deriv_at f (f' x) x) (h' : interval_integrable f' volume a b) : ∫ y in a..b, f' y = f b - f a := integral_eq_sub_of_has_deriv_at h h' open_locale convolution example (f : ℝ → ℝ) (g : ℝ → ℝ) : f ⋆ g = λ x, ∫ t, (f t) * (g (x - t)) := rfl
-
-
-
@@ -1,52 +0,0 @@import analysis.normed_space.finite_dimension import analysis.convolution import measure_theory.function.jacobian import measure_theory.integral.bochner import measure_theory.measure.lebesgue open set filter open_locale topological_space filter ennreal noncomputable theory variables {α : Type*} [measurable_space α] example : measurable_set (∅ : set α) := measurable_set.empty example : measurable_set (univ : set α) := measurable_set.univ example {s : set α} (hs : measurable_set s) : measurable_set sᶜ := hs.compl example : encodable ℕ := by apply_instance example (n : ℕ) : encodable (fin n) := by apply_instance variables {ι : Type*} [encodable ι] example {f : ι → set α} (h : ∀ b, measurable_set (f b)) : measurable_set (⋃ b, f b) := measurable_set.Union h example {f : ι → set α} (h : ∀ b, measurable_set (f b)) : measurable_set (⋂ b, f b) := measurable_set.Inter h open measure_theory variables {μ : measure α} example (s : set α) : μ s = ⨅ t (st : s ⊆ t) (ht : measurable_set t), μ t := measure_eq_infi s example (s : ι → set α) : μ (⋃ i, s i) ≤ ∑' i, μ (s i) := measure_Union_le s example {f : ℕ → set α} (hmeas : ∀ i, measurable_set (f i)) (hdis : pairwise (disjoint on f)) : μ (⋃ i, f i) = ∑' i, μ (f i) := μ.m_Union hmeas hdis example {P : α → Prop} : (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in μ.ae, P x := iff.rfl
-
-
-
@@ -1,68 +0,0 @@import analysis.normed_space.finite_dimension import analysis.convolution import measure_theory.function.jacobian import measure_theory.integral.bochner import measure_theory.measure.lebesgue open set filter open_locale topological_space filter ennreal open measure_theory noncomputable theory variables {α : Type*} [measurable_space α] variables {μ : measure α} section variables {E : Type*} [normed_group E] [normed_space ℝ E] [complete_space E] {f : α → E} example {f g : α → E} (hf : integrable f μ) (hg : integrable g μ) : ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ := integral_add hf hg example {s : set α} (c : E) : ∫ x in s, c ∂μ = (μ s).to_real • c := set_integral_const c example {F : ℕ → α → E} {f : α → E} (bound : α → ℝ) (hmeas : ∀ n, ae_strongly_measurable (F n) μ) (hint : integrable bound μ) (hbound : ∀ n, ∀ᵐ a ∂μ, ∥F n a∥ ≤ bound a) (hlim : ∀ᵐ a ∂μ, tendsto (λ (n : ℕ), F n a) at_top (𝓝 (f a))) : tendsto (λ n, ∫ a, F n a ∂μ) at_top (𝓝 (∫ a, f a ∂μ)) := tendsto_integral_of_dominated_convergence bound hmeas hint hbound hlim example {α : Type*} [measurable_space α] {μ : measure α} [sigma_finite μ] {β : Type*} [measurable_space β] {ν : measure β} [sigma_finite ν] (f : α × β → E) (hf : integrable f (μ.prod ν)) : ∫ z, f z ∂μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ := integral_prod f hf end section open_locale convolution variables {𝕜 : Type*} {G : Type*} {E : Type*} {E' : Type*} {F : Type*} [normed_group E] [normed_group E'] [normed_group F] [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 E'] [normed_space 𝕜 F] [measurable_space G] [normed_space ℝ F] [complete_space F] [has_sub G] example (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : measure G) : f ⋆[L, μ] g = λ x, ∫ t, L (f t) (g (x - t)) ∂μ := rfl end example {E : Type*} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] (μ : measure E) [μ.is_add_haar_measure] {F : Type*}[normed_group F] [normed_space ℝ F] [complete_space F] {s : set E} {f : E → E} {f' : E → (E →L[ℝ] E)} (hs : measurable_set s) (hf : ∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x) (h_inj : inj_on f s) (g : E → F) : ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ := integral_image_eq_integral_abs_det_fderiv_smul μ hs hf h_inj g
-
-
-
@@ -1,9 +0,0 @@import measure_theory.integral.interval_integral import analysis.special_functions.integrals import analysis.convolution open set filter open_locale topological_space filter noncomputable theory
-
-
-
@@ -1,18 +0,0 @@import analysis.normed_space.finite_dimension import analysis.convolution import measure_theory.function.jacobian import measure_theory.integral.bochner import measure_theory.measure.lebesgue open set filter open_locale topological_space filter ennreal noncomputable theory variables {α : Type*} [measurable_space α] variables {ι : Type*} [encodable ι] open measure_theory variables {μ : measure α}
-
-
-
@@ -1,15 +0,0 @@import analysis.normed_space.finite_dimension import analysis.convolution import measure_theory.function.jacobian import measure_theory.integral.bochner import measure_theory.measure.lebesgue open set filter open_locale topological_space filter ennreal open measure_theory noncomputable theory variables {α : Type*} [measurable_space α] variables {μ : measure α}
-