La semana en Calculemus (7 de octubre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En los espacios métricos, d(x,y) ≥ 0
- 2. En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε
- 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 funciones no negativas es no negativo
A continuación se muestran las soluciones.
1. En los espacios métricos, d(x,y) ≥ 0
Demostrar con Lean4 que en los espacios métricos, \(d(x,y) ≥ 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Topology.MetricSpace.Basic variable {X : Type _} [MetricSpace X] variable (x y : X) example : 0 ≤ d x y := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas:
\begin{align}
&0 ≤ ab → 0 < b → 0 ≤ a \tag{L1} \\
&d(x,x) = 0 \tag{L2} \\
&d(x,z) ≤ d(x,y) + d(y,z) \tag{L3} \\
&d(x,y) = d(y,x) \tag{L4} \\
&2a = a + a \tag{L5} \\
&0 < 2 \tag{L6} \\
\end{align}
Por L1 es suficiente demostrar las siguientes desigualdades:
\begin{align}
0 &≤ 2d(x,y) \tag{1} \\
0 &< 2 \tag{2}
\end{align}
La (1) se demuestra por las siguiente cadena de desigualdades:
\begin{align}
0 &= d(x,x) &&\text{[por L2]} \\
&≤ d(x,y) + d(y,x) &&\text{[por L3]} \\
&= d(x,y) + d(x,y) &&\text{[por L4]} \\
&= 2 d(x,y) &&\text{[por L5]}
\end{align}
La (2) se tiene por L6.
Demostraciones con Lean4
|
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 |
import Mathlib.Topology.MetricSpace.Basic variable {X : Type _} [MetricSpace X] variable (x y : X) -- 1ª demostración example : 0 ≤ dist x y := by have h1 : 0 ≤ dist x y * 2 := calc 0 = dist x x := (dist_self x).symm _ ≤ dist x y + dist y x := dist_triangle x y x _ = dist x y + dist x y := by rw [dist_comm x y] _ = dist x y * 2 := (mul_two (dist x y)).symm show 0 ≤ dist x y exact nonneg_of_mul_nonneg_left h1 zero_lt_two -- 2ª demostración example : 0 ≤ dist x y := by apply nonneg_of_mul_nonneg_left . -- 0 ≤ dist x y * 2 calc 0 = dist x x := by simp only [dist_self] _ ≤ dist x y + dist y x := by simp only [dist_triangle] _ = dist x y + dist x y := by simp only [dist_comm] _ = dist x y * 2 := by simp only [mul_two] . -- 0 < 2 exact zero_lt_two -- 3ª demostración example : 0 ≤ dist x y := by have : 0 ≤ dist x y + dist y x := by rw [← dist_self x] apply dist_triangle linarith [dist_comm x y] -- 3ª demostración example : 0 ≤ dist x y := -- by apply? dist_nonneg -- Lemas usados -- ============ -- variable (a b : ℝ) -- variable (z : X) -- #check (dist_comm x y : dist x y = dist y x) -- #check (dist_nonneg : 0 ≤ dist x y) -- #check (dist_self x : dist x x = 0) -- #check (dist_triangle x y z : dist x z ≤ dist x y + dist y z) -- #check (mul_two a : a * 2 = a + a) -- #check (nonneg_of_mul_nonneg_left : 0 ≤ a * b → 0 < b → 0 ≤ a) -- #check (zero_lt_two : 0 < 2) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 22.
2. En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε
Demostrar con Lean4, que en ℝ
\[ \left\{ 0 < ε, ε ≤ 1, |x| < ε, |y| < ε \right\} ⊢ |xy| < ε \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by sorry |
Demostración en lenguaje natural
Se usarán los siguientes lemas
\begin{align}
&|a·b| = |a|·|b| \tag{L1} \\
&0·a = 0 \tag{L2} \\
&0 ≤ |a| \tag{L3} \\
&a ≤ b → a ≠ b → a < b \tag{L4} \\
&a ≠ b ↔ b ≠ a \tag{L5} \\
&0 < a → (ab < ac ↔ b < c) \tag{L6} \\
&0 < a → (ba < ca ↔ b < c) \tag{L7} \\
&0 < a → (ba ≤ ca ↔ b ≤ c) \tag{L8} \\
&1·a = a \tag{L9} \\
\end{align}
Sean \(x, y, ε ∈ ℝ\) tales que
\begin{align}
0 &< ε \tag{he1} \\
ε &≤ 1 \tag{he2} \\
|x| &< ε \tag{hx} \\
|y| &< ε \tag{hy}
\end{align}
y tenemos que demostrar que
\[ |xy| < ε \]
Lo haremos distinguiendo caso según \(|x| = 0\).
1º caso. Supongamos que
\[ |x| = 0 \tag{1} \]
Entonces,
\begin{align}
|xy| &= |x||y| &&\text{[por L1]} \\
&= 0|y| &&\text{[por h1]} \\
&= 0 &&\text{[por L2]} \\
&< ε &&\text{[por he1]}
\end{align}
2º caso. Supongamos que
\[ |x| ≠ 0 \tag{2} \]
Entonces, por L4, L3 y L5, se tiene
\[ 0 < x \tag{3} \]
y, por tanto,
\begin{align}
|xy| &= |x||y| &&\text{[por L1]} \\
&< |x|ε &&\text{[por L6, (3) y (hy)]} \\
&< εε &&\text{[por L7, (he1) y (hx)]} \\
&≤ 1ε &&\text{[por L8, (he1) y (he2)]} \\
&= ε &&\text{[por L9]}
\end{align}
Demostraciones con Lean4
|
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 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 |
import Mathlib.Data.Real.Basic -- 1ª demostración -- =============== example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by intros x y ε he1 he2 hx hy by_cases h : (|x| = 0) . -- h : |x| = 0 show |x * y| < ε calc |x * y| = |x| * |y| := abs_mul x y _ = 0 * |y| := by rw [h] _ = 0 := zero_mul (abs y) _ < ε := he1 . -- h : ¬|x| = 0 have h1 : 0 < |x| := by have h2 : 0 ≤ |x| := abs_nonneg x show 0 < |x| exact lt_of_le_of_ne h2 (ne_comm.mpr h) show |x * y| < ε 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 ε -- 2ª demostración -- =============== example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by intros x y ε he1 he2 hx hy by_cases (|x| = 0) . -- h : |x| = 0 show |x * y| < ε calc |x * y| = |x| * |y| := by apply abs_mul _ = 0 * |y| := by rw [h] _ = 0 := by apply zero_mul _ < ε := by apply he1 . -- h : ¬|x| = 0 have h1 : 0 < |x| := by have h2 : 0 ≤ |x| := by apply abs_nonneg exact lt_of_le_of_ne h2 (ne_comm.mpr h) show |x * y| < ε 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] -- 3ª demostración -- =============== example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by intros x y ε he1 he2 hx hy by_cases (|x| = 0) . -- h : |x| = 0 show |x * y| < ε calc |x * y| = |x| * |y| := by simp only [abs_mul] _ = 0 * |y| := by simp only [h] _ = 0 := by simp only [zero_mul] _ < ε := by simp only [he1] . -- h : ¬|x| = 0 have h1 : 0 < |x| := by have h2 : 0 ≤ |x| := by simp only [abs_nonneg] exact lt_of_le_of_ne h2 (ne_comm.mpr h) show |x * y| < ε calc |x * y| = |x| * |y| := by simp [abs_mul] _ < |x| * ε := by simp only [mul_lt_mul_left, h1, hy] _ < ε * ε := by simp only [mul_lt_mul_right, he1, hx] _ ≤ 1 * ε := by simp only [mul_le_mul_right, he1, he2] _ = ε := by simp only [one_mul] -- Lemas usados -- ============ -- variable (a b c : ℝ) -- #check (abs_mul a b : |a * b| = |a| * |b|) -- #check (abs_nonneg a : 0 ≤ |a|) -- #check (lt_of_le_of_ne : a ≤ b → a ≠ b → a < b) -- #check (mul_le_mul_right : 0 < a → (b * a ≤ c * a ↔ b ≤ c)) -- #check (mul_lt_mul_left : 0 < a → (a * b < a * c ↔ b < c)) -- #check (mul_lt_mul_right : 0 < a → (b * a < c * a ↔ b < c)) -- #check (ne_comm : a ≠ b ↔ b ≠ a) -- #check (one_mul a : 1 * a = a) -- #check (zero_mul a : 0 * a = 0) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 24.
3. La suma de una cota superior de f y una cota superior de g es una cota superior de f+g
Demostrar con Lean4 que si \(f\) y \(g\) son funciones de \(ℝ\) en \(ℝ\), entonces 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 Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic -- (CotaSuperior f a) se verifica si a es una cota superior de f. def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a variable (f g : ℝ → ℝ) variable (a b : ℝ) example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) : CotaSuperior (f + g) (a + b) := by sorry |
Demostración en lenguaje natural
Se usará el siguiente lema
\[ \{a ≤ b, c ≤ d\} \vdash a + c ≤ b + d \tag{L1} \]
Por la definición de cota superior, hay que demostrar que
\[ (∀ x ∈ ℝ) [f(x) + g(x) ≤ a + b] \tag{1} \]
Para ello, sea \(x ∈ R\). Puesto que \(a\) es una cota superior de \(f\), se tiene que
\[ f(x) ≤ a \tag{2} \]
y, puesto que \(b\) es una cota superior de \(g\), se tiene que
\[ g(x) ≤ b \tag{3} \]
De (2) y (3), por L1, se tiene que
\[ f(x) + g(x) ≤ a + b \]
que es lo que había que demostrar.
Demostraciones con Lean4
|
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 69 |
import Mathlib.Data.Real.Basic -- (CotaSuperior f a) se verifica si a es una cota superior de f. def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a variable (f g : ℝ → ℝ) variable (a b : ℝ) -- 1ª demostración -- =============== example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) : CotaSuperior (f + g) (a + b) := by have h1 : ∀ x, (f + g) x ≤ a + b := by { intro x have h2 : f x ≤ a := hfa x have h3 : g x ≤ b := hgb x show (f + g) x ≤ a + b exact add_le_add h2 h3 } show CotaSuperior (f + g) (a + b) exact h1 -- 2ª demostración -- =============== example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) : CotaSuperior (f + g) (a + b) := by have h1 : ∀ x, (f + g) x ≤ a + b := by { intro x show (f + g) x ≤ a + b exact add_le_add (hfa x) (hgb x) } show CotaSuperior (f + g) (a + b) exact h1 -- 3ª demostración -- =============== example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) : CotaSuperior (f + g) (a + b) := by intro x dsimp apply add_le_add . apply hfa . apply hgb -- 4ª demostración -- =============== example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) : CotaSuperior (f + g) (a + b) := λ x ↦ add_le_add (hfa x) (hgb x) -- Lemas usados -- ============ -- variable (c d : ℝ) -- #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 25.
4. La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g
Demostrar con Lean4 que si \(f\) y \(g\) son funciones de \(ℝ\) en \(ℝ\), entonces 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 Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) variable (a b : ℝ) example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by sorry |
Demostración en lenguaje natural
Se usará el siguiente lema
\[ a ≤ b → c ≤ d → a + c ≤ b + d \tag{L1} \]
Por la definición de cota inferior, hay que demostrar que
\[ (∀ x ∈ ℝ) [a + b ≤ f(x) + g(x)] \tag{1} \]
Para ello, sea \(x ∈ R\). Puesto que es \(a\) es una cota inferior de \(f\), se tiene que
\[ a ≤ f(x) \tag{2} \]
y, puesto que \(b\) es una cota inferior de \(g\), se tiene que
\[ b ≤ g(x) \tag{3} \]
De (2) y (3), por L1, se tiene que
\[ a + b ≤ f(x) + g(x) \]
que es lo que había que demostrar.
Demostraciones con Lean4
|
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 |
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) variable (a b : ℝ) -- 1ª demostración example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by 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 exact add_le_add h1a h1b } show CotaInferior (f + g) (a + b) exact h1 -- 2ª demostración example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by have h1 : ∀ x, a + b ≤ f x + g x { intro x show a + b ≤ f x + g x exact add_le_add (hfa x) (hgb x) } show CotaInferior (f + g) (a + b) exact h1 -- 3ª demostración example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by intro x dsimp apply add_le_add . apply hfa . apply hgb -- 4ª demostración example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := λ x ↦ add_le_add (hfa x) (hgb x) -- Lemas usados -- ============ -- variable (c d : ℝ) -- #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 25.
5. El producto de funciones no negativas es no negativo
Demostrar con Lean4 que si \(f\) y \(g\) son funciones no negativas de \(ℝ\) en \(ℝ\), entonces su producto es no negativo.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) example (nnf : CotaInferior f 0) (nng : CotaInferior g 0) : CotaInferior (f * g) 0 := by sorry |
Demostración en lenguaje natural
Se usará el siguiente lema
\[ \{0 ≤ a, 0 ≤ b\} \vdash 0 ≤ ab \tag{L1} \]
Hay que demostrar que
\[ (∀ x ∈ ℝ) [0 ≤ f(x)g(x)] \tag{1} \]
Para ello, sea \(x ∈ R\). Puesto que \(f\) es no negatica, se tiene que
\[ 0 ≤ f(x) \tag{2} \]
y, puesto que \(g\) es no negativa, se tiene que
\[ 0 ≤ g(x) \tag{3} \]
De (2) y (3), por L1, se tiene que
\[ 0 ≤ f(x)g(x) \]
que es lo que había que demostrar.
Demostraciones con Lean4
|
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 |
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) -- 1ª demostración example (nnf : CotaInferior f 0) (nng : CotaInferior g 0) : CotaInferior (f * g) 0 := by 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 exact mul_nonneg h2 h3 } show CotaInferior (f * g) 0 exact h1 -- 2ª demostración example (nnf : CotaInferior f 0) (nng : CotaInferior g 0) : CotaInferior (f * g) 0 := by have h1 : ∀x, 0 ≤ f x * g x { intro x show 0 ≤ f x * g x exact mul_nonneg (nnf x) (nng x) } show CotaInferior (f * g) 0 exact h1 -- 3ª demostración example (nnf : CotaInferior f 0) (nng : CotaInferior g 0) : CotaInferior (f * g) 0 := by intro x dsimp apply mul_nonneg . apply nnf . apply nng -- 4ª demostración example (nnf : CotaInferior f 0) (nng : CotaInferior g 0) : CotaInferior (f * g) 0 := λ x ↦ mul_nonneg (nnf x) (nng x) -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 25.