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.
