-
Notifications
You must be signed in to change notification settings - Fork 0
/
Producto_de_funciones_impares.lean
98 lines (84 loc) · 2.61 KB
/
Producto_de_funciones_impares.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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
-- Producto_de_funciones_impares.lean
-- El producto de dos funciones impares es par
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 16-octubre-2023
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que el producto de dos funciones impares es par.
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Supongamos que f y g son funciones impares. Tenemos que demostrar que
-- f·g es par; 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 impar]
-- = (-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 : esImpar f)
(h2 : esImpar 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 (-x) * g (-x) := neg_mul_neg (f (-x)) (g (-x))
_ = (f * g) (-x) := rfl
-- 2ª demostración
example
(h1 : esImpar f)
(h2 : esImpar 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 (-x) * g (-x) := neg_mul_neg (f (-x)) (g (-x))
_ = (f * g) (-x) := rfl
-- 3ª demostración
example
(h1 : esImpar f)
(h2 : esImpar 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 (-x) * g (-x) := by rw [neg_mul_neg]
_ = (f * g) (-x) := rfl
-- 4ª demostración
example
(h1 : esImpar f)
(h2 : esImpar g)
: esPar (f * g) :=
by
intro x
calc (f * g) x
= f x * g x := rfl
_ = f (-x) * g (-x) := by rw [h1, h2, neg_mul_neg]
_ = (f * g) (-x) := rfl
-- Lemas usados
-- ============
-- variable (a b : ℝ)
-- #check (neg_mul_neg a b : -a * -b = a * b)