El producto de una función par por una impar es impar
Demostrar con Lean4 que el producto de una función par por una impar es impar.
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 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) example (h1 : esPar f) (h2 : esImpar g) : esImpar (f * g) := by sorry |
Demostración en lenguaje natural
Supongamos que \(f\) es una función par y \(g\) lo es impar. Tenemos que demostrar que \(f·g\) es imppar; 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 impar]} \\
&= -f(-x)g(-x)) \\
&= -(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 54 55 56 57 58 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) -- (esPar f) expresa que f es par. def esPar (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x) -- (esImpar f) expresa que f es impar. def esImpar (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x) -- 1ª demostración example (h1 : esPar f) (h2 : esImpar g) : esImpar (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 (-x) * g (-x)) := mul_neg (f (-x)) (g (-x)) _ = -(f * g) (-x) := rfl -- 2ª demostración example (h1 : esPar f) (h2 : esImpar g) : esImpar (f * g) := by intro x calc (f * g) x = f x * g x := rfl _ = f (-x) * -g (-x) := by rw [h1, h2] _ = -(f (-x) * g (-x)) := by rw [mul_neg] _ = -(f * g) (-x) := rfl -- 3ª demostración example (h1 : esPar f) (h2 : esImpar g) : esImpar (f * g) := by intro x calc (f * g) x = f x * g x := rfl _ = -(f (-x) * g (-x)) := by rw [h1, h2, mul_neg] _ = -((f * g) (-x)) := rfl -- Lemas usados -- =========== -- variable (a b : ℝ) -- #check (mul_neg a b : a * -b = -(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. 26.
