Library discprob.basic.Reals_ext
From stdpp Require Import tactics.
From discprob.basic Require Import base order nify.
Require Import Ranalysis5.
Require Import Reals Fourier FunctionalExtensionality.
From Coquelicot Require Export Rcomplements Rbar Series Lim_seq Hierarchy Markov Continuity ElemFct.
Require Import List.
Require Import Psatz Omega.
Lemma Rmult_eq_0_inv_r: ∀ r r1 r2 : R, (r ≠ 0 → r1 = r2) → r × r1 = r × r2.
Lemma Rmult_eq_0_inv_l: ∀ r r1 r2 : R, (r ≠ 0 → r1 = r2) → r1 × r = r2 × r.
Lemma Rmult_neq_0_compat: ∀ r1 r2 : R, r1 ≠ 0 → r2 ≠ 0 → r1 × r2 ≠ 0.
Lemma Rdiv_le_compat_contra: ∀ r1 r2 r3 r4 : R,
0 ≤ r1 → 0 < r4 → r1 ≤ r2 → r4 ≤ r3 → r1 / r3 ≤ r2 / r4.
Lemma Rmult_le_0_compat x y: 0 ≤ x → 0 ≤ y → 0 ≤ x × y.
Lemma fold_right_plus_mult (l: list R) v :
(fold_right Rplus 0 l) × v = fold_right Rplus 0 (map (λ x, x × v) l).
Lemma fold_right_map_Rmult_le {A} (l: list A) f f':
(∀ x, In x l → 0 ≤ f x ∧ f x ≤ f' x) →
fold_right Rmult 1 (map f l) ≤ fold_right Rmult 1 (map f' l).
Hint Resolve Rabs_pos Rle_ge.
Lemma Rabs_case r (P : R → Type):
(0 ≤ r → P r) → (0 ≤ -r → P (-r)) → P (Rabs r).
Lemma open_interval_open x y :
open (open_interval x y).
Lemma disc_ball z Δ x:
disc z Δ x ↔ ball z Δ x.
Lemma open_included_disc U z:
open U → U z → ∃ delta : posreal, included (disc z delta) U.
Lemma open_open_set U:
open U → open_set U.
Lemma disc_neighbourhood x (δ: posreal):
neighbourhood (disc x δ) x.
Lemma ball_neighbourhood x (δ: R):
δ > 0 →
neighbourhood (ball x δ) x.
Lemma pos_INR': ∀ n : nat, (0 < n)%nat → 0 < INR n.
Lemma archimed_rat_dense1 eps r:
0 < eps →
0 ≤ r →
∃ n m, r < INR n / INR m < r + eps ∧ (0 < m)%nat.
Lemma archimed_rat_dense2 eps r:
0 < eps →
r < 0 →
∃ n m, r < - INR n / INR m < r + eps ∧ (0 < m)%nat.
Lemma is_lim_seq_plus_inv un vn u v:
is_lim_seq (λ n, un n + vn n) (u + v) →
is_lim_seq (λ n, vn n) v →
is_lim_seq (λ n, un n) u.
Lemma is_lim_seq_opp_inv un u:
is_lim_seq (λ n, - un n) (- u) →
is_lim_seq (λ n, un n) u.
Lemma Rmin_diff_eq x y:
Rmin x y = (x + y) / 2 - Rabs(x - y) / 2.
Lemma Rmax_diff_eq x y:
Rmax x y = (x + y) / 2 + Rabs(x - y) / 2.
Lemma continuous_Rmin_l x y: continuous (Rmin x) y.
Lemma continuous_Rmax_l x y: continuous (Rmax x) y.
Lemma archimed_pos r: 0 ≤ r → ∃ n, INR n ≤ r < INR (S n).
Lemma pow_INR n k: INR (n^k) = INR n^k.
Lemma INR_diff_lt_1_eq n k: 0 ≤ INR n - INR k < 1 → n = k.
Lemma Sup_seq_const k: Sup_seq (λ n, k) = k.
Lemma Sup_seq_real (xn: nat → R): Rbar_lt m_infty (Sup_seq xn).
Lemma Sup_seq_real_p_infty (xn: nat → R):
Sup_seq xn = p_infty ↔ ∀ k, ∃ n, k ≤ xn n.
Definition Rbar_max (x y: Rbar) : Rbar :=
match x, y with
| Finite x', Finite y' ⇒ Rmax x' y'
| m_infty, _ ⇒ y
| _, m_infty ⇒ x
| p_infty, _ ⇒ p_infty
| _, p_infty ⇒ p_infty
end.
Lemma Rbar_max_l: ∀ x y : Rbar, Rbar_le x (Rbar_max x y).
Lemma Rbar_max_r: ∀ x y : Rbar, Rbar_le y (Rbar_max x y).
Lemma Rbar_max_comm: ∀ x y : Rbar, Rbar_max x y = Rbar_max y x.
Lemma Rbar_max_case: ∀ (x y : Rbar) (P : Rbar → Type), P x → P y → P (Rbar_max x y).
Lemma Rbar_max_case_strong:
∀ (x y : Rbar) (P : Rbar → Type),
(Rbar_le y x → P x) → (Rbar_le x y → P y) → P (Rbar_max x y).
Lemma norm_Rabs r: norm r = Rabs r.
From discprob.basic Require Import base order nify.
Require Import Ranalysis5.
Require Import Reals Fourier FunctionalExtensionality.
From Coquelicot Require Export Rcomplements Rbar Series Lim_seq Hierarchy Markov Continuity ElemFct.
Require Import List.
Require Import Psatz Omega.
Lemma Rmult_eq_0_inv_r: ∀ r r1 r2 : R, (r ≠ 0 → r1 = r2) → r × r1 = r × r2.
Lemma Rmult_eq_0_inv_l: ∀ r r1 r2 : R, (r ≠ 0 → r1 = r2) → r1 × r = r2 × r.
Lemma Rmult_neq_0_compat: ∀ r1 r2 : R, r1 ≠ 0 → r2 ≠ 0 → r1 × r2 ≠ 0.
Lemma Rdiv_le_compat_contra: ∀ r1 r2 r3 r4 : R,
0 ≤ r1 → 0 < r4 → r1 ≤ r2 → r4 ≤ r3 → r1 / r3 ≤ r2 / r4.
Lemma Rmult_le_0_compat x y: 0 ≤ x → 0 ≤ y → 0 ≤ x × y.
Lemma fold_right_plus_mult (l: list R) v :
(fold_right Rplus 0 l) × v = fold_right Rplus 0 (map (λ x, x × v) l).
Lemma fold_right_map_Rmult_le {A} (l: list A) f f':
(∀ x, In x l → 0 ≤ f x ∧ f x ≤ f' x) →
fold_right Rmult 1 (map f l) ≤ fold_right Rmult 1 (map f' l).
Hint Resolve Rabs_pos Rle_ge.
Lemma Rabs_case r (P : R → Type):
(0 ≤ r → P r) → (0 ≤ -r → P (-r)) → P (Rabs r).
Lemma open_interval_open x y :
open (open_interval x y).
Lemma disc_ball z Δ x:
disc z Δ x ↔ ball z Δ x.
Lemma open_included_disc U z:
open U → U z → ∃ delta : posreal, included (disc z delta) U.
Lemma open_open_set U:
open U → open_set U.
Lemma disc_neighbourhood x (δ: posreal):
neighbourhood (disc x δ) x.
Lemma ball_neighbourhood x (δ: R):
δ > 0 →
neighbourhood (ball x δ) x.
Lemma pos_INR': ∀ n : nat, (0 < n)%nat → 0 < INR n.
Lemma archimed_rat_dense1 eps r:
0 < eps →
0 ≤ r →
∃ n m, r < INR n / INR m < r + eps ∧ (0 < m)%nat.
Lemma archimed_rat_dense2 eps r:
0 < eps →
r < 0 →
∃ n m, r < - INR n / INR m < r + eps ∧ (0 < m)%nat.
Lemma is_lim_seq_plus_inv un vn u v:
is_lim_seq (λ n, un n + vn n) (u + v) →
is_lim_seq (λ n, vn n) v →
is_lim_seq (λ n, un n) u.
Lemma is_lim_seq_opp_inv un u:
is_lim_seq (λ n, - un n) (- u) →
is_lim_seq (λ n, un n) u.
Lemma Rmin_diff_eq x y:
Rmin x y = (x + y) / 2 - Rabs(x - y) / 2.
Lemma Rmax_diff_eq x y:
Rmax x y = (x + y) / 2 + Rabs(x - y) / 2.
Lemma continuous_Rmin_l x y: continuous (Rmin x) y.
Lemma continuous_Rmax_l x y: continuous (Rmax x) y.
Lemma archimed_pos r: 0 ≤ r → ∃ n, INR n ≤ r < INR (S n).
Lemma pow_INR n k: INR (n^k) = INR n^k.
Lemma INR_diff_lt_1_eq n k: 0 ≤ INR n - INR k < 1 → n = k.
Lemma Sup_seq_const k: Sup_seq (λ n, k) = k.
Lemma Sup_seq_real (xn: nat → R): Rbar_lt m_infty (Sup_seq xn).
Lemma Sup_seq_real_p_infty (xn: nat → R):
Sup_seq xn = p_infty ↔ ∀ k, ∃ n, k ≤ xn n.
Definition Rbar_max (x y: Rbar) : Rbar :=
match x, y with
| Finite x', Finite y' ⇒ Rmax x' y'
| m_infty, _ ⇒ y
| _, m_infty ⇒ x
| p_infty, _ ⇒ p_infty
| _, p_infty ⇒ p_infty
end.
Lemma Rbar_max_l: ∀ x y : Rbar, Rbar_le x (Rbar_max x y).
Lemma Rbar_max_r: ∀ x y : Rbar, Rbar_le y (Rbar_max x y).
Lemma Rbar_max_comm: ∀ x y : Rbar, Rbar_max x y = Rbar_max y x.
Lemma Rbar_max_case: ∀ (x y : Rbar) (P : Rbar → Type), P x → P y → P (Rbar_max x y).
Lemma Rbar_max_case_strong:
∀ (x y : Rbar) (P : Rbar → Type),
(Rbar_le y x → P x) → (Rbar_le x y → P y) → P (Rbar_max x y).
Lemma norm_Rabs r: norm r = Rabs r.