Skip to main content

La suma de dos funciones pares es par

Demostrar con Lean4 que la suma de dos funciones pares es par.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- (esPar f) expresa que f es par.
def esPar (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

example
  (h1 : esPar f)
  (h2 : esPar g)
  : esPar (f + g) :=
by sorry

Demostración en lenguaje natural

Supongamos que \(f\) y \(g\) son funciones pares. Tenemos que demostrar que \(f+g\) es par; es decir, que \[ (∀ x ∈ ℝ) [(f + g)(x) = (f + g)(-x)] \] Sea \(x ∈ ℝ\). Entonces, \begin{align} (f + g) x &= f(x) + g(x) \newline &= f(-x) + g(x) &&\text{[porque \(f\) es par]} \newline &= f(-x) + g(-x) &&\text{[porque \(g\) es par]} \newline &= (f + g)(-x) \end{align}

Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- (esPar f) expresa que f es par.
def esPar (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

-- 1ª demostración
-- ===============

example
  (h1 : esPar f)
  (h2 : esPar g)
  : esPar (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 + g) (-x)    := rfl

-- 2ª demostración
-- ===============

example
  (h1 : esPar f)
  (h2 : esPar g)
  : esPar (f + g) :=
by
  intro x
  calc (f + g) x
       = f x + g x       := rfl
     _ = f (-x) + g x    := congrArg (. + g x) (h1 x)
     _ = f (-x) + g (-x) := congrArg (f (-x) + .) (h2 x)
     _ = (f + g) (-x)    := rfl

-- 3ª demostración
-- ===============

example
  (h1 : esPar f)
  (h2 : esPar g)
  : esPar (f + g) :=
by
  intro x
  calc (f + g) x
       = f x + g x       := rfl
     _ = f (-x) + g (-x) := by rw [h1, h2]
     _ = (f + g) (-x)    := rfl

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias