La semana en Calculemus (5 de noviembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. La suma de dos funciones acotadas superiormente también lo está
- 2. La suma de dos funciones acotadas inferiormente también lo está
- 3. Si a es una cota superior de f y c ≥ 0, entonces ca es una cota superior de cf
- 4. Si c ≥ 0 y f está acotada superiormente, entonces c·f también lo está
- 5. Si x e y son sumas de dos cuadrados, entonces xy también lo es
A continuación se muestran las soluciones.
1. La suma de dos funciones acotadas superiormente también lo está
Demostrar con Lean4 que la suma de dos funciones acotadas superiormente también lo está.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import src.Suma_de_cotas_superiores variable {f g : ℝ → ℝ} -- (acotadaSup f) afirma que f tiene cota superior. def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a example (hf : acotadaSup f) (hg : acotadaSup g) : acotadaSup (f + g) := by sorry |
Demostración en lenguaje natural
Del ejercicio La suma de una cota superior de f y una cota superior de g es una cota superior de f+g usaremos la definición de cota superior (CotaSuperior) y el lema sumaCotaSup.
Puesto que \(f\) está acotada superiormente, tiene una cota superior. Sea \(a\) una de dichas cotas. Análogamentte, puesto que \(g\) está acotada superiormente, tiene una cota superior. Sea \(b\) una de dichas cotas. Por el lema sumaCotaSup, \(a+b\) es una cota superior de \(f+g\). Por consiguiente, \(f+g\) está acotada superiormente.
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 |
import src.Suma_de_cotas_superiores variable {f g : ℝ → ℝ} -- (acotadaSup f) afirma que f tiene cota superior. def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a -- 1ª demostración example (hf : acotadaSup f) (hg : acotadaSup g) : acotadaSup (f + g) := by cases' hf with a ha -- a : ℝ -- ha : CotaSuperior f a cases' hg with b hb -- b : ℝ -- hb : CotaSuperior g b have h1 : CotaSuperior (f + g) (a + b) := sumaCotaSup ha hb have h2 : ∃ z, CotaSuperior (f+g) z := Exists.intro (a + b) h1 show acotadaSup (f + g) exact h2 -- 2ª demostración example (hf : acotadaSup f) (hg : acotadaSup g) : acotadaSup (f + g) := by cases' hf with a ha -- a : ℝ -- ha : FnUb f a cases' hg with b hb -- b : ℝ -- hb : FnUb g b use a + b apply sumaCotaSup ha hb -- 4ª demostración example (hf : acotadaSup f) (hg : acotadaSup g) : acotadaSup (f + g) := by rcases hf with ⟨a, ha⟩ rcases hg with ⟨b, hb⟩ exact ⟨a + b, sumaCotaSup ha hb⟩ -- 5ª demostración example : acotadaSup f → acotadaSup g → acotadaSup (f + g) := by rintro ⟨a, ha⟩ ⟨b, hb⟩ exact ⟨a + b, sumaCotaSup ha hb⟩ -- 6ª demostración example : acotadaSup f → acotadaSup g → acotadaSup (f + g) := fun ⟨a, ha⟩ ⟨b, hb⟩ ↦ ⟨a + b, sumaCotaSup ha hb⟩ -- Lemas usados -- ============ -- #check (sumaCotaSup : CotaSuperior f a → CotaSuperior g b → CotaSuperior (f + g) (a + b)) |
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 29.
2. La suma de dos funciones acotadas inferiormente también lo está
Demostrar con Lean4 que la suma de dos funciones acotadas inferiormente también lo está.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import src.Suma_de_cotas_inferiores variable {f g : ℝ → ℝ} -- (acotadaInf f) afirma que f tiene cota inferior. def acotadaInf (f : ℝ → ℝ) := ∃ a, CotaInferior f a example (hf : acotadaInf f) (hg : acotadaInf g) : acotadaInf (f + g) := by sorry |
Demostración en lenguaje natural
Del ejercicio “La suma de una cota inferior de \(f\) y una cota inferior de \(g\) es una cota inferior de \(f+g\)” usaremos la definición de cota inferior (CotaInferior) y el lema sumaCotaInf.
Puesto que \(f\) está acotada inferiormente, tiene una cota inferior. \(a\) una de dichas cotas. Análogamentte, puesto que \(g\) está acotada inferiormente, tiene una cota inferior. Sea \(b\) una de dichas cotas. Por el lema sumaCotaInf, a+b es una cota inferior de \(f+g\). Por consiguiente, \(f+g\) está acotada inferiormente.
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 |
import src.Suma_de_cotas_inferiores variable {f g : ℝ → ℝ} -- (acotadaInf f) afirma que f tiene cota inferior. def acotadaInf (f : ℝ → ℝ) := ∃ a, CotaInferior f a -- 1ª demostración example (hf : acotadaInf f) (hg : acotadaInf g) : acotadaInf (f + g) := by cases' hf with a ha -- a : ℝ -- ha : CotaInferior f a cases' hg with b hb -- b : ℝ -- hb : CotaInferior g b have h1 : CotaInferior (f + g) (a + b) := sumaCotaInf ha hb have h2 : ∃ z, CotaInferior (f + g) z := Exists.intro (a + b) h1 show acotadaInf (f + g) exact h2 -- 2ª demostración example (hf : acotadaInf f) (hg : acotadaInf g) : acotadaInf (f + g) := by cases' hf with a ha -- a : ℝ -- ha : FnLb f a cases' hg with b hgb -- b : ℝ -- hgb : FnLb g b use a + b -- ⊢ FnLb (f + g) (a + b) apply sumaCotaInf ha hgb -- 3ª demostración example (hf : acotadaInf f) (hg : acotadaInf g) : acotadaInf (f + g) := by rcases hf with ⟨a, ha⟩ -- a : ℝ -- ha : FnLb f a rcases hg with ⟨b, hb⟩ -- b : ℝ -- hb : FnLb g b exact ⟨a + b, sumaCotaInf ha hb⟩ -- 4ª demostración example : acotadaInf f → acotadaInf g → acotadaInf (f + g) := by rintro ⟨a, ha⟩ ⟨b, hb⟩ -- a : ℝ -- ha : FnLb f a -- b : ℝ -- hb : FnLb g b exact ⟨a + b, sumaCotaInf ha hb⟩ -- 5ª demostración example : acotadaInf f → acotadaInf g → acotadaInf (f + g) := fun ⟨a, ha⟩ ⟨b, hb⟩ ↦ ⟨a + b, sumaCotaInf ha hb⟩ -- Lemas usados -- ============ -- #check (sumaCotaInf : FnLb f a → FnLb g b → FnLb (f + g) (a + b)) |
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 29.
3. Si a es una cota superior de f y c ≥ 0, entonces ca es una cota superior de cf
Demostrar con Lean4 que si \(a\) es una cota superior de \(f\) y \(c ≥ 0\), entonces \(ca\) es una cota superior de \(cf\).
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 : ℝ → ℝ} variable {c : ℝ} example (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := by sorry |
Demostración en lenguaje natural
Se usará el lema
\[ \{b ≤ c, 0 ≤ a\} ⊢ ab ≤ ac \tag{L1} \]
Tenemos que demostrar que
\[ (∀ y ∈ ℝ) cf(y) ≤ ca \]
Sea \(y ∈ R\). Puesto que \(a\) es una cota de \(f\), se tiene que
\[ f(y) ≤ a \]
que, junto con \(c ≥ 0\), por el lema L1 nos da
\[ cf(y) ≤ ca \]
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 |
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 : ℝ → ℝ} variable {c : ℝ} -- 1ª demostración example (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := by intro y -- y : ℝ -- ⊢ (fun x => c * f x) y ≤ c * a have ha : f y ≤ a := hfa y calc (fun x => c * f x) y = c * f y := by rfl _ ≤ c * a := mul_le_mul_of_nonneg_left ha h -- 2ª demostración example (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := by intro y calc (fun x => c * f x) y = c * f y := by rfl _ ≤ c * a := mul_le_mul_of_nonneg_left (hfa y) h -- 3ª demostración example (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := by intro y show (fun x => c * f x) y ≤ c * a exact mul_le_mul_of_nonneg_left (hfa y) h -- 4ª demostración lemma CotaSuperior_mul (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := fun y ↦ mul_le_mul_of_nonneg_left (hfa y) h -- Lemas usados -- ============ -- variable (c : ℝ) -- #check (mul_le_mul_of_nonneg_left : b ≤ c → 0 ≤ a → a * b ≤ a * c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 29.
4. Si c ≥ 0 y f está acotada superiormente, entonces c·f también lo está
Demostrar con Lean4 que si \(c ≥ 0\) y \(f\) está acotada superiormente, entonces \(c·f\) también lo está.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import src.Cota_superior_de_producto_por_escalar variable {f : ℝ → ℝ} variable {c : ℝ} -- (acotadaSup f) afirma que f tiene cota superior. def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a example (hf : acotadaSup f) (hc : c ≥ 0) : acotadaSup (fun x ↦ c * f x) := by sorry |
Demostración en lenguaje natural
Usaremos el siguiente lema:
\begin{align}
“\text{Si } a \text{ es cota superior de } f \text{ y } c ≥ 0\text{, entonces } c·a \text{ es cota superior de } c·f”
\end{align}
Puesto que \(f\) está acotada superiormente, tiene una cota superior. Sea \(a\) una de dichas cotas. Entonces, por el lema, \(c·a\) es una cota superior de \(c·f\). Por consiguiente, \(c·f\) está acotada superiormente.
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 src.Cota_superior_de_producto_por_escalar variable {f : ℝ → ℝ} variable {c : ℝ} -- (acotadaSup f) afirma que f tiene cota superior. def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a -- 1ª demostración example (hf : acotadaSup f) (hc : c ≥ 0) : acotadaSup (fun x ↦ c * f x) := by cases' hf with a ha -- a : ℝ -- ha : CotaSuperior f a have h1 : CotaSuperior (fun x ↦ c * f x) (c * a) := CotaSuperior_mul ha hc have h2 : ∃ z, ∀ x, (fun x ↦ c * f x) x ≤ z := Exists.intro (c * a) h1 show acotadaSup (fun x ↦ c * f x) exact h2 -- 2ª demostración example (hf : acotadaSup f) (hc : c ≥ 0) : acotadaSup (fun x ↦ c * f x) := by cases' hf with a ha -- a : ℝ -- ha : CotaSuperior f a use c * a -- ⊢ CotaSuperior (fun x => c * f x) (c * a) apply CotaSuperior_mul ha hc -- 3ª demostración example (hf : acotadaSup f) (hc : c ≥ 0) : acotadaSup (fun x ↦ c * f x) := by rcases hf with ⟨a, ha⟩ -- a : ℝ -- ha : CotaSuperior f a exact ⟨c * a, CotaSuperior_mul ha hc⟩ -- 4ª demostración example (hc : c ≥ 0) : acotadaSup f → acotadaSup (fun x ↦ c * f x) := by rintro ⟨a, ha⟩ -- a : ℝ -- ha : CotaSuperior f a exact ⟨c * a, CotaSuperior_mul ha hc⟩ -- 5ª demostración example (hc : c ≥ 0) : acotadaSup f → acotadaSup (fun x ↦ c * f x) := fun ⟨a, ha⟩ ↦ ⟨c * a, CotaSuperior_mul ha hc⟩ -- Lemas usados -- ============ -- #check (CotaSuperior_mul : CotaSuperior f a → c ≥ 0 → CotaSuperior (fun x ↦ c * f x) (c * a)) |
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 29.
5. Si x e y son sumas de dos cuadrados, entonces xy también lo es
Demostrar con Lean4 que si \(x\) e \(y\) son sumas de dos cuadrados, entonces \(xy\) también lo es
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.Tactic variable {α : Type _} [CommRing α] variable {x y : α} -- (suma_de_cuadrados x) afirma que x se puede escribir como la suma -- de dos cuadrados. def suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2 example (hx : suma_de_cuadrados x) (hy : suma_de_cuadrados y) : suma_de_cuadrados (x * y) := by sorry |
Demostración en lenguaje natural
Puesto que \(x\) e \(y\) se pueden escribir como la suma de dos cuadrados, existen \(a\), \(b\) , \(c\) y \(d\) tales que
\begin{align}
x &= a² + b² \\
y &= c² + d²
\end{align}
Entonces,
\begin{align}
xy &= (a² + b²)(c² + d²) \\
&= a²c² + b²d² + a²d² + b²c² \\
&= a²c² – 2acbd + b²d² + a²d² + 2adbc + b²c² \\
&= (ac – bd)² + (ad + bc)²
\end{align}
Por tanto, \(xy\) es la suma de dos cuadrados.
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 |
import Mathlib.Tactic variable {α : Type _} [CommRing α] variable {x y : α} -- (suma_de_cuadrados x) afirma que x se puede escribir como la suma -- de dos cuadrados. def suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2 -- 1ª demostración example (hx : suma_de_cuadrados x) (hy : suma_de_cuadrados y) : suma_de_cuadrados (x * y) := by rcases hx with ⟨a, b, xeq : x = a^2 + b^2⟩ -- a b : α -- xeq : x = a ^ 2 + b ^ 2 rcases hy with ⟨c, d, yeq : y = c^2 + d^2⟩ -- c d : α -- yeq : y = c ^ 2 + d ^ 2 have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2 := calc x * y = (a^2 + b^2) * (c^2 + d^2) := by rw [xeq, yeq] _ = a^2*c^2 + b^2*d^2 + a^2*d^2 + b^2*c^2 := by ring _ = a^2*c^2 - 2*a*c*b*d + b^2*d^2 + a^2*d^2 + 2*a*d*b*c + b^2*c^2 := by ring _ = (a*c - b*d)^2 + (a*d + b*c)^2 := by ring have h2 : ∃ f, x * y = (a*c - b*d)^2 + f^2 := Exists.intro (a*d + b*c) h1 have h3 : ∃ e f, x * y = e^2 + f^2 := Exists.intro (a*c - b*d) h2 show suma_de_cuadrados (x * y) exact h3 -- 2ª demostración example (hx : suma_de_cuadrados x) (hy : suma_de_cuadrados y) : suma_de_cuadrados (x * y) := by rcases hx with ⟨a, b, xeq : x = a^2 + b^2⟩ -- a b : α -- xeq : x = a ^ 2 + b ^ 2 rcases hy with ⟨c, d, yeq : y = c^2 + d^2⟩ -- c d : α -- yeq : y = c ^ 2 + d ^ 2 have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2 := calc x * y = (a^2 + b^2) * (c^2 + d^2) := by rw [xeq, yeq] _ = (a*c - b*d)^2 + (a*d + b*c)^2 := by ring have h2 : ∃ e f, x * y = e^2 + f^2 := by tauto show suma_de_cuadrados (x * y) exact h2 -- 3ª demostración example (hx : suma_de_cuadrados x) (hy : suma_de_cuadrados y) : suma_de_cuadrados (x * y) := by rcases hx with ⟨a, b, xeq⟩ -- a b : α -- xeq : x = a ^ 2 + b ^ 2 rcases hy with ⟨c, d, yeq⟩ -- c d : α -- yeq : y = c ^ 2 + d ^ 2 rw [xeq, yeq] -- ⊢ suma_de_cuadrados ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2)) use a*c - b*d, a*d + b*c -- ⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) -- = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2 ring -- 4ª demostración example (hx : suma_de_cuadrados x) (hy : suma_de_cuadrados y) : suma_de_cuadrados (x * y) := by rcases hx with ⟨a, b, rfl⟩ -- ⊢ suma_de_cuadrados ((a ^ 2 + b ^ 2) * y) rcases hy with ⟨c, d, rfl⟩ -- ⊢ suma_de_cuadrados ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2)) use a*c - b*d, a*d + b*c -- ⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) -- = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2 ring |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 30.