DAO: La semana en Calculemus (11 de noviembre de 2022)
Esta semana he publicado en Calculemus las demostraciones con Lean 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 a·b es una cota superior de f·g
- 2. La suma de dos funciones monótonas es monótona
- 3. Si f es monótona y c ≥ 0, entonces c·f 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 a·b es una cota superior de f·g
Demostrar 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 a·b 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 15 16 17 18 |
import data.real.basic def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x variables (f g : ℝ → ℝ) variables (a b : ℝ) example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (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 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 data.real.basic def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x variables (f g : ℝ → ℝ) variables (a b : ℝ) -- 1ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := begin 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, by exact mul_le_mul h2 h3 h4 nna, }, show cota_superior (f * g) (a * b), by exact h1, end -- 2ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := begin intro x, change f x * g x ≤ a * b, apply mul_le_mul, apply hfa, apply hgb, apply nng, apply nna end -- 3ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := begin dunfold cota_superior no_negativa at *, intro x, have h1:= hfa x, have h2:= hgb x, have h3:= nng x, exact mul_le_mul h1 h2 h3 nna, end -- 4ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := begin dunfold cota_superior no_negativa at *, intro x, specialize hfa x, specialize hgb x, specialize nng x, exact mul_le_mul hfa hgb nng nna, end -- 5ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := λ x, mul_le_mul (hfa x) (hgb x) (nng x) nna |
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.
2. La suma de dos funciones monótonas es monótona
Demostrar que la suma de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import data.real.basic variables (f g : ℝ → ℝ) example (mf : monotone f) (mg : monotone g) : monotone (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 : ℝ → ℝ) -- 1ª demostración -- =============== example (mf : monotone f) (mg : monotone g) : monotone (f + g) := begin 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), by exact h1, end -- 2ª demostración -- =============== example (mf : monotone f) (mg : monotone g) : monotone (f + g) := begin intros a b hab, apply add_le_add, apply mf hab, apply mg hab end -- 3ª demostración -- =============== example (mf : monotone f) (mg : monotone g) : monotone (f + g) := λ a b hab, add_le_add (mf hab) (mg hab) |
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. 28.
3. Si f es monótona y c ≥ 0, entonces c·f es monótona
Demostrar que si f es monótona y c ≥ 0, entonces c·f es monótona.
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 : ℝ → ℝ) variable {c : ℝ} example (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := 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 |
import data.real.basic variables (f : ℝ → ℝ) variable {c : ℝ} -- 1ª demostración -- =============== example (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := begin have h1 : ∀ a b, a ≤ b → (λ x, c * f x) a ≤ (λ x, c * f x) b, { intros a b hab, have h2 : f a ≤ f b := mf hab, have h3 : c * f a ≤ c * f b := mul_le_mul_of_nonneg_left h2 nnc, show (λ x, c * f x) a ≤ (λ x, c * f x) b, by exact h3, }, show monotone (λ x, c * f x), by exact h1, end -- 2ª demostración -- =============== example (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := begin intros a b hab, apply mul_le_mul_of_nonneg_left, apply mf hab, apply nnc end -- 3ª demostración -- =============== example (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := λ a b hab, mul_le_mul_of_nonneg_left (mf hab) nnc |
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. 28.
4. La composición de dos funciones monótonas es monótona
Demostrar que la composición de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import data.real.basic variables (f g : ℝ → ℝ) example (mf : monotone f) (mg : monotone g) : monotone (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 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 |
import data.real.basic variables (f g : ℝ → ℝ) -- 1ª demostración -- =============== example (mf : monotone f) (mg : monotone g) : monotone (f ∘ g) := begin have h1 : ∀ a b, a ≤ b → (f ∘ g) a ≤ (f ∘ g) b, { intros a b hab, have h1 : g a ≤ g b := mg hab, have h2 : f (g a) ≤ f (g b) := mf h1, show (f ∘ g) a ≤ (f ∘ g) b, by exact h2, }, show monotone (f ∘ g), by exact h1, end -- 2ª demostración -- =============== example (mf : monotone f) (mg : monotone g) : monotone (f ∘ g) := begin intros a b hab, apply mf, apply mg, apply hab end -- 3ª demostración -- =============== example (mf : monotone f) (mg : monotone g) : monotone (f ∘ g) := λ a b hab, mf (mg hab) -- 4ª demostración -- =============== example (mf : monotone f) (mg : monotone g) : monotone (f ∘ g) := -- by library_search monotone.comp mf mg -- 5ª demostración -- =============== example (mf : monotone f) (mg : monotone g) : monotone (f ∘ g) := -- by hint by tauto |
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. 28.
5. La suma de dos funciones pares es par
La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x).
Demostrar que la suma de dos funciones pares es par.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic variables (f g : ℝ → ℝ) def par (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) example (hf : par f) (hg : par g) : par (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 |
import data.real.basic variables (f g : ℝ → ℝ) def par (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- 1ª demostración -- =============== example (hf : par f) (hg : par g) : par (f + g) := begin intro x, have h1 : f x = f (-x) := hf x, have h2 : g x = g (-x) := hg x, calc (f + g) x = f x + g x : rfl ... = f (-x) + g x : congr_arg (+ g x) h1 ... = f (-x) + g (-x) : congr_arg ((+) (f (-x))) h2 ... = (f + g) (-x) : rfl end -- 2ª demostración -- =============== example (hf : par f) (hg : par g) : par (f + g) := begin intro x, calc (f + g) x = f x + g x : rfl ... = f (-x) + g (-x) : by rw [hf, hg] ... = (f + g) (-x) : rfl 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. 28.