{"id":1686,"date":"2023-10-13T06:00:35","date_gmt":"2023-10-13T04:00:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1686"},"modified":"2023-10-10T12:47:39","modified_gmt":"2023-10-10T10:47:39","slug":"13-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/13-oct-23\/","title":{"rendered":"La suma de dos funciones pares es par"},"content":{"rendered":"

Demostrar con Lean4 que la suma de dos funciones pares es par.<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- (esPar f) expresa que f es par.\ndef esPar (f : \u211d \u2192 \u211d) : Prop :=\n  \u2200 x, f x = f (-x)\n\nexample\n  (h1 : esPar f)\n  (h2 : esPar g)\n  : esPar (f + g) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nSupongamos que \(f\) y \(g\) son funciones pares. Tenemos que demostrar que \(f+g\) es par; es decir, que
\n\[ (\u2200 x \u2208 \u211d) [(f + g)(x) = (f + g)(-x)] \]
\nSea \(x \u2208 \u211d\). Entonces,
\n\begin{align}
\n   (f + g) x &= f(x) + g(x)   \\
\n             &= f(-x) + g(x)  &&\text{[porque \(f\) es par]} \\
\n             &= f(-x) + g(-x) &&\text{[porque \(g\) es par]} \\
\n             &= (f + g)(-x)
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- (esPar f) expresa que f es par.\ndef esPar (f : \u211d \u2192 \u211d) : Prop :=\n  \u2200 x, f x = f (-x)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : esPar f)\n  (h2 : esPar g)\n  : esPar (f + g) :=\nby\n  intro x\n  have h1 : f x = f (-x) := h1 x\n  have h2 : g x = g (-x) := h2 x\n  calc (f + g) x\n       = f x + g x       := rfl\n     _ = f (-x) + g x    := congrArg (. + g x) h1\n     _ = f (-x) + g (-x) := congrArg (f (-x) + .) h2\n     _ = (f + g) (-x)    := rfl\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : esPar f)\n  (h2 : esPar g)\n  : esPar (f + g) :=\nby\n  intro x\n  calc (f + g) x\n       = f x + g x       := rfl\n     _ = f (-x) + g x    := congrArg (. + g x) (h1 x)\n     _ = f (-x) + g (-x) := congrArg (f (-x) + .) (h2 x)\n     _ = (f + g) (-x)    := rfl\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : esPar f)\n  (h2 : esPar g)\n  : esPar (f + g) :=\nby\n  intro x\n  calc (f + g) x\n       = f x + g x       := rfl\n     _ = f (-x) + g (-x) := by rw [h1, h2]\n     _ = (f + g) (-x)    := rfl\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n