-
Notifications
You must be signed in to change notification settings - Fork 0
/
Producto_funcion_par_e_impar.lean
84 lines (71 loc) · 2.25 KB
/
Producto_funcion_par_e_impar.lean
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
-- Producto_funcion_par_e_impar.lean
-- El producto de una función par por una impar es impar
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 17-octubre-2023
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que el producto de una función par por una impar es impar.
-- ----------------------------------------------------------------------
-- 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,
-- (f·g) x = f(x)g(x)
-- = f(-x)g(x) [porque f es par]
-- = f(-x)(-g(-x)) [porque g es impar]
-- = -f(-x)g(-x))
-- = -(f·g)(-x)
-- 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)
-- (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))