Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Reg.v Sprache: Lisp

Original von: Coq^©

Require Import Reals.

Axiom y : R -> R.
Axiom d_y : derivable y.
Axiom n_y : forall x : R, y x <> 0%R.
Axiom dy_0 : derive_pt y 0 (d_y 0%R) = 1%R.

Lemma essai0 : continuity_pt (fun x : R => ((x + 2) / y x + x / y x)%R) 0.
assert (H := d_y).
assert (H0 := n_y).
reg.
Qed.

Lemma essai1 : derivable_pt (fun x : R => (/ 2 * sin x)%R) 1.
reg.
Qed.

Lemma essai2 : continuity (fun x : R => (Rsqr x * cos (x * x) + x)%R).
reg.
Qed.

Lemma essai3 : derivable_pt (fun x : R => (x * (Rsqr x + 3))%R) 0.
reg.
Qed.

Lemma essai4 : derivable (fun x : R => ((x + x) * sin x)%R).
reg.
Qed.

Lemma essai5 : derivable (fun x : R => (1 + sin (2 * x + 3) * cos (cos x))%R).
reg.
Qed.

Lemma essai6 : derivable (fun x : R => cos (x + 3)).
reg.
Qed.

Lemma essai7 :
derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1.
reg.
apply Rlt_0_1.
red; intro;  rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0;
assumption.
Qed.

Lemma essai8 : derivable_pt (fun x : R => sqrt (Rsqr x + sin x + 1)) 0.
reg.
rewrite sin_0.
rewrite Rsqr_0.
replace (0 + 0 + 1)%R with 1%R; [ apply Rlt_0_1 |  ring ].
Qed.

Lemma essai9 : derivable_pt (id + sin) 1.
reg.
Qed.

Lemma essai10 : derivable_pt (fun x : R => (x + 2)%R) 0.
reg.
Qed.

Lemma essai11 : derive_pt (fun x : R => (x + 2)%R) 0 essai10 = 1%R.
reg.
Qed.

Lemma essai12 : derivable (fun x : R => (x + Rsqr (x + 2))%R).
reg.
Qed.

Lemma essai13 :
derive_pt (fun x : R => (x + Rsqr (x + 2))%R) 0 (essai12 0%R) = 5%R.
reg.
Qed.

Lemma essai14 : derivable_pt (fun x : R => (2 * x + x)%R) 2.
reg.
Qed.

Lemma essai15 : derive_pt (fun x : R => (2 * x + x)%R) 2 essai14 = 3%R.
reg.
Qed.

Lemma essai16 : derivable_pt (fun x : R => (x + sin x)%R) 0.
reg.
Qed.

Lemma essai17 : derive_pt (fun x : R => (x + sin x)%R) 0 essai16 = 2%R.
reg.
rewrite cos_0.
reflexivity.
Qed.

Lemma essai18 : derivable_pt (fun x : R => (x + y x)%R) 0.
assert (H := d_y).
reg.
Qed.

Lemma essai19 : derive_pt (fun x : R => (x + y x)%R) 0 essai18 = 2%R.
assert (H := dy_0).
assert (H0 := d_y).
reg.
Qed.

Axiom z : R -> R.
Axiom d_z : derivable z.

Lemma essai20 : derivable_pt (fun x : R => z (y x)) 0.
reg.
apply d_y.
apply d_z.
Qed.

Lemma essai21 : derive_pt (fun x : R => z (y x)) 0 essai20 = 1%R.
assert (H := dy_0).
reg.
Abort.

Lemma essai22 : derivable (fun x : R => (sin (z x) + Rsqr (z x) / y x)%R).
assert (H := d_y).
reg.
apply n_y.
apply d_z.
Qed.

(* Pour tester la continuite de sqrt en 0 *)
Lemma essai23 :
continuity_pt
   (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1.
reg.
left; apply Rlt_0_1.
right; unfold Rminus;  rewrite Rplus_opp_r; reflexivity.
Qed.

Lemma essai24 :
derivable (fun x : R => (sqrt (x * x + 2 * x + 2) + Rabs (x * x + 1))%R).
reg.
replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R.
apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ].
unfold Rsqr;  ring.
red; intro; cut (0 < x * x + 1)%R.
intro;  rewrite H in H0; elim (Rlt_irrefl _ H0).
apply Rplus_le_lt_0_compat;
[  replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ]
| apply Rlt_0_1 ].
Qed.

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.