La semana en Calculemus (14 de octubre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces ab es una cota superior de fg
- 2. La suma de dos funciones monótonas es monótona
- 3. Si c es no negativo y f es monótona, entonces cf es monótona
- 4. La composición de dos funciones monótonas es monótona
- 5. La suma de dos funciones pares es par
A continuación se muestran las soluciones.
1. Si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces ab es una cota superior de fg
Sean \(f\) y \(g\) funciones de \(ℝ\) en \(ℝ\). Demostrar con Lean4 que si \(a\) es una cota superior no negativa de \(f\) y \(b\) es es una cota superior de la función no negativa \(g\), entonces \(ab\) es una cota superior de \(fg\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 |
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 -- (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 : CotaSuperior f a) (hgb : CotaSuperior g b) (nng : CotaInferior g 0) (nna : 0 ≤ a) : CotaSuperior (f * g) (a * b) := by sorry |
Demostración en lenguaje natural
Se usará el siguiente lema
\[ \{a ≤ b, c ≤ d, 0 ≤ c, 0 ≤ b\} ⊢ ac ≤ bd \tag{L1} \]
Hay que demostrar que
\[ (∀ x ∈ ℝ) [f(x)g(x) ≤ ab] \tag{1} \]
Para ello, sea \(x ∈ R\). Puesto que \(a\) es una cota superior de \(f\), se tiene que
\[ f(x) ≤ a \tag{2} \]
puesto que \(b\) es una cota superior de \(g\), se tiene que
\[ g(x) ≤ b \tag{3} \]
puesto que \(g\) es no negativa, se tiene que
\[ 0 ≤ g(x) \tag{4} \]
y, puesto que \(a\) es no negativo, se tiene que
\[ 0 ≤ a \tag{5} \]
De (2), (3), (4) y (5), por L1, se tiene que
\[ f(x)g(x) ≤ ab \]
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 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 |
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 -- (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 : CotaSuperior f a) (hgb : CotaSuperior g b) (nng : CotaInferior g 0) (nna : 0 ≤ a) : CotaSuperior (f * g) (a * b) := by have h1 : ∀ x, f x * g x ≤ a * b { intro x have h2 : f x ≤ a := hfa x have h3 : g x ≤ b := hgb x have h4 : 0 ≤ g x := nng x show f x * g x ≤ a * b exact mul_le_mul h2 h3 h4 nna } show CotaSuperior (f * g) (a * b) exact h1 -- 2ª demostración example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) (nng : CotaInferior g 0) (nna : 0 ≤ a) : CotaSuperior (f * g) (a * b) := by intro x dsimp apply mul_le_mul . apply hfa . apply hgb . apply nng . apply nna -- 3ª demostración example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) (nng : CotaInferior g 0) (nna : 0 ≤ a) : CotaSuperior (f * g) (a * b) := by intro x have h1:= hfa x have h2:= hgb x have h3:= nng x exact mul_le_mul h1 h2 h3 nna -- 4ª demostración example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) (nng : CotaInferior g 0) (nna : 0 ≤ a) : CotaSuperior (f * g) (a * b) := by intro x specialize hfa x specialize hgb x specialize nng x exact mul_le_mul hfa hgb nng nna -- 5ª demostración example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) (nng : CotaInferior g 0) (nna : 0 ≤ a) : CotaSuperior (f * g) (a * b) := λ x ↦ mul_le_mul (hfa x) (hgb x) (nng x) nna -- Lemas usados -- ============ -- variable (c d : ℝ) -- #check (mul_le_mul : a ≤ b → c ≤ d → 0 ≤ c → 0 ≤ b → 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.
2. La suma de dos funciones monótonas es monótona
Demostrar con Lean4 que la suma de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) example (mf : Monotone f) (mg : Monotone g) : Monotone (f + g) := by sorry |
Demostración en lenguaje natural
Se usará el siguiente lema:
\[ \{a ≤ b, c ≤ d\} ⊢ a + c ≤ b + d \tag{L1} \]
Supongamos que \(f\) y \(g\) son monótonas y teneno que demostrar que \(f+g\) también lo es; que
\[ (∀ a,\ b \in ℝ) [a ≤ b → (f + g)(a) ≤ (f + g)(b)] \]
Sean \(a, b ∈ ℝ\) tales que
\[ a ≤ b \tag{1} \]
Entonces, por ser \(f\) y \(g\) monótonas se tiene
\begin{align}
f(a) &≤ f(b) \tag{2} \\
g(a) &≤ g(b) \tag{3}
\end{align}
Entonces,
\begin{align}
(f + g)(a) &= f(a) + g(a) \\
&≤ f(b) + g(b) &&\text{[por L1, (2) y (3)]} \\
&= (f + g)(b)
\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 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- 1ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f + g) := by have h1 : ∀ a b, a ≤ b → (f + g) a ≤ (f + g) b { intros a b hab have h2 : f a ≤ f b := mf hab have h3 : g a ≤ g b := mg hab calc (f + g) a = f a + g a := rfl _ ≤ f b + g b := add_le_add h2 h3 _ = (f + g) b := rfl } show Monotone (f + g) exact h1 -- 2ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f + g) := by have h1 : ∀ a b, a ≤ b → (f + g) a ≤ (f + g) b { intros a b hab calc (f + g) a = f a + g a := rfl _ ≤ f b + g b := add_le_add (mf hab) (mg hab) _ = (f + g) b := rfl } show Monotone (f + g) exact h1 -- 3ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f + g) := by have h1 : ∀ a b, a ≤ b → (f + g) a ≤ (f + g) b { intros a b hab show (f + g) a ≤ (f + g) b exact add_le_add (mf hab) (mg hab) } show Monotone (f + g) exact h1 -- 4ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f + g) := by -- a b : ℝ -- hab : a ≤ b intros a b hab apply add_le_add . -- f a ≤ f b apply mf hab . -- g a ≤ g b apply mg hab -- 5ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f + g) := λ _ _ hab ↦ add_le_add (mf hab) (mg hab) -- Lemas usados -- ============ -- variable (a b 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. 26.
3. Si c es no negativo y f es monótona, entonces cf es monótona
Demostrar con Lean4 que si \(c\) es no negativo y \(f\) es monótona, entonces \(cf\) es monótona.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable {c : ℝ} example (mf : Monotone f) (nnc : 0 ≤ c) : Monotone (fun x ↦ c * f x) := by sorry |
Demostración en lenguaje natural
Se usará el Lema
\[ \{b ≤ c, 0 ≤ a\} ⊢ ab ≤ ac \tag{L1} \]
Tenemos que demostrar que
\[ (∀ a, b ∈ ℝ) [a ≤ b → (cf)(a) ≤ (cf)(b)] \]
Sean \(a, b ∈ ℝ\) tales que \(a ≤ b\). Puesto que \(f\) es monótona, se tiene
\[ f(a) ≤ f(b) \]
y, junto con la hipótesis de que \(c\) es no negativo, usando el lema L1, se tiene que
\[ cf(a) ≤ cf(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 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable {c : ℝ} -- 1ª demostración example (mf : Monotone f) (nnc : 0 ≤ c) : Monotone (fun x ↦ c * f x) := by have h1 : ∀ a b, a ≤ b → (fun x ↦ c * f x) a ≤ (fun x ↦ c * f x) b { intros a b hab have h2 : f a ≤ f b := mf hab show (fun x ↦ c * f x) a ≤ (fun x ↦ c * f x) b exact mul_le_mul_of_nonneg_left h2 nnc } show Monotone (fun x ↦ c * f x) exact h1 -- 2ª demostración example (mf : Monotone f) (nnc : 0 ≤ c) : Monotone (fun x ↦ c * f x) := by -- a b : ℝ -- hab : a ≤ b intros a b hab -- (fun x => c * f x) a ≤ (fun x => c * f x) b apply mul_le_mul_of_nonneg_left . -- f a ≤ f b apply mf hab . -- 0 ≤ c apply nnc -- 3ª demostración example (mf : Monotone f) (nnc : 0 ≤ c) : Monotone (fun x ↦ c * f x) := λ _ _ hab ↦ mul_le_mul_of_nonneg_left (mf hab) nnc -- Lemas usados -- ============ -- variable (a b : ℝ) -- #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. 26.
4. La composición de dos funciones monótonas es monótona
Demostrar con Lean4 que la composición de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) example (mf : Monotone f) (mg : Monotone g) : Monotone (f ∘ g) := by sorry |
Demostración en lenguaje natural
Sean \(f\) y \(g\) dos funciones monótonas de \(ℝ\) en \(ℝ\). Tenemos que demostrar que \(f ∘ g\) es monótona; es decir, que
\[ (∀ a, b ∈ ℝ) [a ≤ b → (f ∘ g)(a) ≤ (f ∘ g)(b)] \]
Sean \(a, b ∈ ℝ\) tales que \(a ≤ b\). Por ser \(g\) monótona, se tiene
\[ g(a) ≤ g(b) \]
y, por ser f monótona, se tiene
\[ f(g(a)) ≤ f(g(b)) \]
Finalmente, por la definición de composición,
\[ (f ∘ g)(a) ≤ (f ∘ g)(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 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- 1ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f ∘ g) := by have h1 : ∀ a b, a ≤ b → (f ∘ g) a ≤ (f ∘ g) b { intros a b hab have h1 : g a ≤ g b := mg hab show (f ∘ g) a ≤ (f ∘ g) b exact mf h1 } show Monotone (f ∘ g) exact h1 -- 2ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f ∘ g) := by have h1 : ∀ a b, a ≤ b → (f ∘ g) a ≤ (f ∘ g) b { intros a b hab show (f ∘ g) a ≤ (f ∘ g) b exact mf (mg hab) } show Monotone (f ∘ g) exact h1 -- 3ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f ∘ g) := by -- a b : ℝ -- hab : a ≤ b intros a b hab -- (f ∘ g) a ≤ (f ∘ g) b apply mf -- g a ≤ g b apply mg -- a ≤ b apply hab -- 4ª demostración example (mf : Monotone f) (mg : Monotone g) : Monotone (f ∘ g) := λ _ _ hab ↦ mf (mg hab) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 26.
5. La suma de dos funciones pares es par
Demostrar con Lean4 que la suma de dos funciones pares es par.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) example (h1 : esPar f) (h2 : esPar g) : esPar (f + g) := by sorry |
Demostración en lenguaje natural
Supongamos que \(f\) y \(g\) son funciones pares. Tenemos que demostrar que \(f+g\) es par; es decir, que
\[ (∀ x ∈ ℝ) [(f + g)(x) = (f + g)(-x)] \]
Sea \(x ∈ ℝ\). Entonces,
\begin{align}
(f + g) x &= f(x) + g(x) \\
&= f(-x) + g(x) &&\text{[porque \(f\) es par]} \\
&= f(-x) + g(-x) &&\text{[porque \(g\) es par]} \\
&= (f + g)(-x)
\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 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- 1ª demostración -- =============== example (h1 : esPar f) (h2 : esPar g) : esPar (f + g) := by intro x have h1 : f x = f (-x) := h1 x have h2 : g x = g (-x) := h2 x calc (f + g) x = f x + g x := rfl _ = f (-x) + g x := congrArg (. + g x) h1 _ = f (-x) + g (-x) := congrArg (f (-x) + .) h2 _ = (f + g) (-x) := rfl -- 2ª demostración -- =============== example (h1 : esPar f) (h2 : esPar g) : esPar (f + g) := by intro x calc (f + g) x = f x + g x := rfl _ = f (-x) + g x := congrArg (. + g x) (h1 x) _ = f (-x) + g (-x) := congrArg (f (-x) + .) (h2 x) _ = (f + g) (-x) := rfl -- 3ª demostración -- =============== example (h1 : esPar f) (h2 : esPar g) : esPar (f + g) := by intro x calc (f + g) x = f x + g x := rfl _ = f (-x) + g (-x) := by rw [h1, h2] _ = (f + g) (-x) := rfl |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 26.