DAO: La semana en Calculemus (4 de noviembre de 2022)
Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:
- 1. Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0
- 2. Si x, y, ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε
- 3. La suma de una cota superior de f y una cota superior de g es una cota superior de f+g
- 4. La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g
- 5. El producto de dos funciones no negativas es no negativa
A continuación se muestran las soluciones.
1. Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0
Demostrar que si X es un espacio métrico y x, y ∈ X, entonces
|
1 |
0 ≤ dist x y |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import topology.metric_space.basic variables {X : Type*} [metric_space X] variables x y : X example : 0 ≤ dist x y := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 |
import topology.metric_space.basic variables {X : Type*} [metric_space X] variables x y : X -- 1ª demostración example : 0 ≤ dist x y := have h1 : 2 * dist x y ≥ 0, by calc 2 * dist x y = dist x y + dist x y : two_mul (dist x y) ... = dist x y + dist y x : by rw [dist_comm x y] ... ≥ dist x x : dist_triangle x y x ... = 0 : dist_self x, show 0 ≤ dist x y, by exact nonneg_of_mul_nonneg_left h1 zero_lt_two -- 2ª demostración example : 0 ≤ dist x y := -- by library_search dist_nonneg |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 24.
2. Si x,y,ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε
Demostrar que si x,y,ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import data.real.basic tactic example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 |
import data.real.basic tactic -- 1ª demostración -- =============== example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := begin intros x y ε he1 he2 hx hy, by_cases h : (|x| = 0), { calc |x * y| = |x| * |y| : abs_mul x y ... = 0 * |y| : by rw h ... = 0 : zero_mul (abs y) ... < ε : he1 }, { have h1 : 0 < |x|, { have h2 : 0 ≤ |x| := abs_nonneg x, show 0 < |x|, exact lt_of_le_of_ne h2 (ne.symm h) }, calc |x * y| = |x| * |y| : abs_mul x y ... < |x| * ε : (mul_lt_mul_left h1).mpr hy ... < ε * ε : (mul_lt_mul_right he1).mpr hx ... ≤ 1 * ε : (mul_le_mul_right he1).mpr he2 ... = ε : one_mul ε }, end -- 2ª demostración -- =============== example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := begin intros x y ε he1 he2 hx hy, by_cases h : (|x| = 0), { calc |x * y| = |x| * |y| : by apply abs_mul ... = 0 * |y| : by rw h ... = 0 : by apply zero_mul ... < ε : by apply he1 }, { have h1 : 0 < |x|, { have h2 : 0 ≤ |x|, apply abs_nonneg, exact lt_of_le_of_ne h2 (ne.symm h) }, calc |x * y| = |x| * |y| : by rw abs_mul ... < |x| * ε : by apply (mul_lt_mul_left h1).mpr hy ... < ε * ε : by apply (mul_lt_mul_right he1).mpr hx ... ≤ 1 * ε : by apply (mul_le_mul_right he1).mpr he2 ... = ε : by rw [one_mul] }, end -- 3ª demostración -- =============== example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := begin intros x y ε he1 he2 hx hy, by_cases (|x| = 0), { by finish }, { have : 0 < |x|, by finish, calc |x * y| = |x| * |y| : by rw abs_mul ... < |x| * ε : by finish ... ≤ 1 * ε : by nlinarith ... = ε : by finish }, end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 26.
3. La suma de una cota superior de f y una cota superior de g es una cota superior de f+g
Demostrar que la suma de una cota superior de f y una cota superior de g es una cota superior de f+g.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import data.real.basic -- (cota_superior f a) se verifica si a es una cota superior de f. def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a variables (f g : ℝ → ℝ) variables (a b : ℝ) example (hfa : cota_superior f a) (hgb : cota_superior g b) : cota_superior (λ x, f x + g x) (a + b) := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 |
import data.real.basic -- (cota_superior f a) se verifica si a es una cota superior de f. def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a variables (f g : ℝ → ℝ) variables (a b : ℝ) -- 1ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) : cota_superior (λ x, f x + g x) (a + b) := begin have h1 : ∀ x, f x + g x ≤ a + b, { intro x, have h1a : f x ≤ a := hfa x, have h1b : g x ≤ b := hgb x, show f x + g x ≤ a + b, by exact add_le_add (hfa x) (hgb x), }, show cota_superior (λ x, f x + g x) (a + b), by exact h1, end -- 2ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) : cota_superior (λ x, f x + g x) (a + b) := begin intro x, dsimp, change f x + g x ≤ a + b, apply add_le_add, apply hfa, apply hgb end -- 3ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) : cota_superior (λ x, f x + g x) (a + b) := λ x, add_le_add (hfa x) (hgb x) |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 27.
4. La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g
Demostrar que la suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import data.real.basic -- (cota_inferior f a) se verifica si a es una cota inferior de f. def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variables (f g : ℝ → ℝ) variables (a b : ℝ) example (hfa : cota_inferior f a) (hgb : cota_inferior g b) : cota_inferior (λ x, f x + g x) (a + b) := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 |
import data.real.basic -- (cota_inferior f a) se verifica si a es una cota inferior de f. def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variables (f g : ℝ → ℝ) variables (a b : ℝ) -- 1ª demostración -- =============== example (hfa : cota_inferior f a) (hgb : cota_inferior g b) : cota_inferior (λ x, f x + g x) (a + b) := begin have h1 : ∀ x, a + b ≤ f x + g x, { intro x, have h1a : a ≤ f x := hfa x, have h1b : b ≤ g x := hgb x, show a + b ≤ f x + g x, by exact add_le_add (hfa x) (hgb x), }, show cota_inferior (λ x, f x + g x) (a + b), by exact h1, end -- 2ª demostración -- =============== example (hfa : cota_inferior f a) (hgb : cota_inferior g b) : cota_inferior (λ x, f x + g x) (a + b) := begin intro x, dsimp, change a + b ≤ f x + g x, apply add_le_add, apply hfa, apply hgb end -- 3ª demostración -- =============== example (hfa : cota_inferior f a) (hgb : cota_inferior g b) : cota_inferior (λ x, f x + g x) (a + b) := λ x, add_le_add (hfa x) (hgb x) |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 27.
5. El producto de dos funciones no negativas es no negativa
Demostrar que el producto de dos funciones no negativas es no negativa.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import data.real.basic variables (f g : ℝ → ℝ) def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x example (nnf : no_negativa f) (nng : no_negativa g) : no_negativa (f * g) := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 |
import data.real.basic variables (f g : ℝ → ℝ) def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x -- 1ª demostración -- =============== example (nnf : no_negativa f) (nng : no_negativa g) : no_negativa (f * g) := begin have h1 : ∀x, 0 ≤ f x * g x, { intro x, have h2: 0 ≤ f x := nnf x, have h3: 0 ≤ g x := nng x, show 0 ≤ f x * g x, by exact mul_nonneg (nnf x) (nng x), }, show no_negativa (f * g), by exact h1, end -- 2ª demostración -- =============== example (nnf : no_negativa f) (nng : no_negativa g) : no_negativa (f * g) := begin intro x, change 0 ≤ f x * g x, apply mul_nonneg, apply nnf, apply nng end -- 3ª demostración -- =============== example (nnf : no_negativa f) (nng : no_negativa g) : no_negativa (f * g) := λ x, mul_nonneg (nnf x) (nng x) |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 27.