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.
