Nombres réels 3 : La valeur absolue et la distance sur les réels
La valeur absolue : Rabs
Vous connaissez certainement la valeur absolue. Dans un cours de mathématiques, la valeur absolue d'un réel x est le réel noté |x| défini par : |x| = -x si x < 0 x si x >= 0. En fait il y a certainement mille façon de définir la valeur absolue, mais ce qui importe ici, c'est que cette fonction s'appelle Rabs et qu'on admet les deux théorèmes suivants :
Pour prouver des choses sur Rabs, le plus souvent on raisonne par cas.
Voici un exemple important :
remarquer (Rlt_or_le x 0) : x < 0 ∨ 0 ≤ x.
Theorem Rabs_pos : ∀ x : R, 0 ≤ Rabs x.
Proof.
intros x.
destruct (Rlt_or_le x 0) as [I | I].
- (* x < 0 *)
left.
rewrite Rabs_left.
(* On utilise le fait que l'opposé est une fonction strictement
décroissante. *)
+ rewrite <-Ropp_0.
apply Ropp_lt_contravar.
exact I.
+ exact I.
- (* 0 <= x *)
rewrite Rabs_pos_eq by (exact I). exact I.
Qed.
Deux remarques importantes sur la preuve précédente :
La preuve de x < 0 -> 0 < -x va nous servir souvent, en fait c'est :
- Nous avons utilisé rewrite avec un énoncé du type :
x < 0 → Rabs x = - x.
- dans le but, Rabs x est remplacé par -x;
- vous continuez votre preuve;
- à la fin, Coq vous demande de prouver que x < 0.
- la deuxième fois on a fourni directment la preuve que 0 ≤ x avec
Exercice : Prouver le théorème suivant.
Theorem Ropp_gt_lt_0_contravar : ∀ r : R, r < 0 → - r > 0.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem Rle_abs : ∀ x : R, x ≤ Rabs x.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem Rabs_R0 : Rabs 0 = 0.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Petit détour par la fonction carré
Exercice : Prouver le théorème suivant.
Theorem Rsqr_neg (x : R) : x² = (- x)².
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Check Rmult_gt_0_lt_compat.
Check Rmult_gt_0_compat.
Theorem Rsqr_incrst_1 : ∀ x y : R, x < y → 0 ≤ x → 0 ≤ y → x² < y².
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Check Rmult_gt_0_compat.
Theorem Rsqr_incrst_1 : ∀ x y : R, x < y → 0 ≤ x → 0 ≤ y → x² < y².
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem Rsqr_inj : ∀ x y : R, 0 ≤ x → 0 ≤ y → x² = y² → x = y.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Valeur absolue et carré
Exercice : Prouver le théorème suivant.
On se souvient qu'un carré est toujours positif :
et que le carré est invariant par opposé :
Check Rsqr_neg.
Theorem Rabs_sqr (x : R) : Rabs (x²) = (Rabs x)².
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem Rabs_sqr (x : R) : Rabs (x²) = (Rabs x)².
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem Rabs_Ropp : ∀ x : R, Rabs (- x) = Rabs x.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Pour le prochain exercice, il y a deux stratégies différentes :
- séparer en 4 cas suivant le signe de x et de y
- ou bien passer par la fonction carré
Theorem Rabs_mult : ∀ x y : R, Rabs (x × y) = Rabs x × Rabs y.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Dans le prochain exercice, et les suivants, vous pourrez utiliser :
Exercice : Prouver le théorème suivant.
Bon... celui-ci est assez pénible à la main, vous avez le droit de le passer.
Theorem Rsqr_plus: ∀ x y : R, (x + y)² = x² + y² + 2 × x × y.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Ici, vous pourrez utiliser :
Theorem Rabs_triang : ∀ a b, Rabs (a + b) ≤ Rabs a + Rabs b.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Print Rdist.
Dans un cours de mathématique, elle est définie par
d(x, y) = |y - x|.
Remarque culturelle au passage : généralement, en mathématiques, une
distance sur un ensemble E est une fonction d de E * E dans l'ensemble des
réels positifs ou nuls qui satisfait :
Nous concluons cette partie par une preuve de ces faits.
Pour passer de ≤ à ≥ facilement (et réciproquement), on a:
- symétrie : d(x, y) = d(y, x)
- séparation : d(x, y) = 0 <-> x = y
- inégalité triangulaire : d(x, z) <= d(x, y) + d(y, x).
Exercice : Prouver le théorème suivant.
Ici, c'est juste Reals qui nous embête avec ≥.
Penser à unfold Rdist
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Admitted. (* Remplacer cette ligne par Qed. *)
Penser à unfold Rdist et unfold Rminus
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem Rabs_eq_0 : ∀ x, Rabs x = 0 ↔ x = 0.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem Rdist_refl (x y : R) : Rdist x y = 0 ↔ x = y.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)