CoRN.ode.BanachFixpoint
Require Import
QArith
stdlib_rationals Qinf Qpossec QposInf QnonNeg abstract_algebra QType_rationals additional_operations.
Require Import Qauto QOrderedType.
Require Import theory.rings theory.dec_fields orders.rings orders.dec_fields nat_pow.
Require Import interfaces.naturals interfaces.orders.
Import peano_naturals.
Require Import CRGeometricSum.
Import Qround Qpower.
Require Import metric.
Local Notation ball := mspc_ball.
Local Notation "x ²" := (x × x) (at level 30) : mc_scope.
Section BanachFixpoint.
Add Field Q : (stdlib_field_theory Q).
Context `{MetricSpaceClass X} {Xlim : Limit X} {Xcms : CompleteMetricSpaceClass X}.
Context (f : X → X) `{!IsContraction f q} (x0 : X).
Let x n := nat_iter n f x0.
Arguments x n%mc.
Lemma x_Sn : ∀ n, x (1 + n) = f (x n).
Proof. reflexivity. Qed.
Let d := msd (x 0) (x 1).
Instance : PropHolds (0 ≤ d).
Proof. apply msd_nonneg. Qed.
Instance : PropHolds (0 ≤ q).
Proof. apply (lip_nonneg f q).
Qed.
Instance : PropHolds (q < 1).
Proof. apply (contr_lt_1 f q). Qed.
Instance : PropHolds (0 < 1 - q).
Proof.
assert (A := contr_lt_1 f q).
rewrite <- flip_lt_negate in A. apply (strictly_order_preserving (1 +)) in A.
now rewrite plus_negate_r in A.
Qed.
Global Instance : ∀ q : Q, PropHolds (0 < q) → PropHolds (q ≠ 0).
Proof. apply lt_ne_flip. Qed.
Lemma dist_xn_xSn : ∀ n : nat, ball (d × q^n) (x n) (x (1 + n)).
Proof.
induction n using nat_induction.
+ rewrite nat_pow_0, right_identity; subst d; apply mspc_distance.
+ rewrite nat_pow_S. mc_setoid_replace (d × (q × q ^ n)) with (q × (d × q^n)) by ring.
change (x (1 + n)) with (f (x n)); change (x (1 + (1 + n))) with (f (x (1 + n))).
now apply contr_prf.
Qed.
Lemma dist_xm_xn : ∀ m n : nat, ball (d × q^m × (1 - q^n) / (1 - q)) (x m) (x (m + n)).
Proof.
intro m; induction n as [| n IH] using nat_induction.
+ rewrite right_identity; apply mspc_refl.
now rewrite nat_pow_0, plus_negate_r, right_absorb, left_absorb.
+ apply (mspc_triangle' (d × q^m × (1 - q^n) / (1 - q))%mc (d × q^(m + n))%mc (x (m + n))); trivial.
- rewrite nat_pow_S, nat_pow_exp_plus. field; solve_propholds.
- mc_setoid_replace (m + (1 + n)) with (1 + (m + n)) by ring. apply dist_xn_xSn.
Qed.
Lemma dist_xm_xn' : ∀ m n : nat, ball (d × q^m / (1 - q)) (x m) (x (m + n)).
Proof.
intros m n. apply (mspc_monotone (d × q^m × (1 - q^n) / (1 - q))%mc); [| apply dist_xm_xn].
apply (order_preserving (.* /(1 - q))). rewrite <- associativity.
apply (order_preserving (d *.)). rewrite <- (mult_1_r (q^m)) at 2.
apply (order_preserving (q^m *.)). rewrite <- (plus_0_r 1) at 2.
apply (order_preserving (1 +)). rewrite <- negate_0.
apply flip_le_negate. solve_propholds.
Qed.
Lemma Qpower_mc_power (e : Q) (n : nat) : (e ^ n)%Q = (e ^ n)%mc.
Proof.
induction n as [| n IH] using nat_induction.
+ now rewrite nat_pow_0.
+ rewrite Nat2Z.inj_add, Qpower_plus'.
- now rewrite nat_pow_S, IH.
- rewrite <- Nat2Z.inj_add; change 0%Z with (Z.of_nat 0); rewrite Nat2Z.inj_iff;
apply not_eq_sym, O_S.
Qed.
Lemma Qstepl : ∀ (x y z : Q), x ≤ y → x = z → z ≤ y.
Proof. intros ? ? ? ? A2; now rewrite <- A2. Qed.
Lemma Qstepr : ∀ (x y z : Q), x ≤ y → y = z → x ≤ z.
Proof. intros ? ? ? ? A2; now rewrite <- A2. Qed.
Declare Left Step Qstepl.
Declare Right Step Qstepr.
Lemma binom_ineq (a : Q) (n : nat) : -1 ≤ a → 1 + (n : Q) × a ≤ (1 + a)^n.
Proof.
intro A.
assert (A1 : 0 ≤ 1 + a) by (now apply (order_preserving (1 +)) in A; rewrite plus_negate_r in A).
induction n as [| n IH] using nat_induction.
+ rewrite nat_pow_0; change (1 + 0 × a ≤ 1); now rewrite mult_0_l, plus_0_r.
+ rewrite nat_pow_S. transitivity ((1 + a) × (1 + (n : Q) × a)).
- rewrite Nat2Z.inj_add, inject_Z_plus.
stepr (1 + (1 + (n : Q)) × a + (n : Q) × a²) by ring.
apply nonneg_plus_le_compat_r. apply nonneg_mult_compat; [solve_propholds | apply square_nonneg].
- now apply (order_preserving ((1 + a) *.)) in IH.
Qed.
Lemma nat_pow_recip `{DecField A} `{Naturals B} `{!NatPowSpec A B pw} :
(∀ x y : A, Decision (x = y)) →
∀ (a : A) (n : B), (/a) ^ n = /(a ^ n).
Proof.
intros D a. apply naturals.induction.
+ intros n1 n2 E; now rewrite E.
+ rewrite !nat_pow_0; symmetry; apply dec_recip_1.
+ intros n IH. now rewrite !nat_pow_S, dec_recip_distr, IH.
Qed.
Lemma power_tends_to_zero (e : Q) (n : nat) :
0 < e → Z.to_nat (Qceiling (/(e × (1 - q)))%mc) ≤ n → q ^ n ≤ e.
Proof.
intros A1 A2.
assert (A3 : 0 < n).
+ let T := type of A2 in match T with (?lhs ≤ _) ⇒ apply lt_le_trans with (y := lhs) end; [| trivial].
apply Q.Qlt_lt_of_nat_inject_Z; change (0 < / (e × (1 - q))); solve_propholds.
+ destruct n as [| n]; [elim (lt_irrefl _ A3) |].
rewrite <- Qpower_mc_power.
apply GeometricCovergenceLemma with (e := e ↾ A1); [solve_propholds .. |].
apply (Q.le_Qle_Qceiling_to_nat _ (S n)), A2.
Qed.
Lemma const_x (N : Q → nat) : d = 0 → cauchy x N.
Proof.
intro eq_d_0.
assert (A := mspc_distance (x 0) (x 1)).
subst d; rewrite eq_d_0 in A.
assert (C : ∀ n, x n = x 0).
+ induction n as [| n IH] using nat_induction; [easy |].
change (x (1 + n)) with (f (x n)). rewrite IH. symmetry; apply A.
+ intros e e_pos m n _ _. rewrite (C m), (C n). apply mspc_refl. solve_propholds.
Qed.
Lemma cauchy_x : cauchy x (λ e, Z.to_nat (Qceiling (d / (e × (1 - q)²))%mc)).
Proof.
assert (d_nonneg : 0 ≤ d) by solve_propholds.
assert (d_pos_0 : 0 = d ∨ 0 < d) by now apply le_equiv_lt.
destruct d_pos_0 as [d_0 | d_pos]; [now apply const_x |].
intros e e_pos.
match goal with
|- ∀ m n, @?G m n ⇒ intros m n; assert (A : ∀ m n, m ≤ n → G m n)
end.
+ clear m n; intros m n le_m_n A _.
rewrite <- (cut_minus_le n m); trivial. rewrite plus_comm.
apply (mspc_monotone (d × q^m / (1 - q))%mc); [| apply dist_xm_xn'].
cut (q ^ m ≤ e × (1 - q) / d).
- intro A1. apply (order_preserving (d *.)), (order_preserving (.* /(1 - q))) in A1.
apply (po_proper' A1); [easy | field; split; solve_propholds].
- apply power_tends_to_zero; [solve_propholds |].
apply (po_proper' A); [| easy]. apply f_equal, Qceiling_comp.
match goal with |- (Qeq ?l ?r) ⇒ change (l = r) end.
field; repeat split; solve_propholds.
+ assert (A1 : TotalRelation (A := nat) (≤)) by apply _; destruct (A1 m n).
- now apply A.
- intros; apply mspc_symm; now apply A.
Qed.
Definition fp := lim (reg_fun x _ cauchy_x).
Lemma banach_fixpoint : f fp = fp.
Proof.
assert (C := cauchy_x).
eapply (iter_fixpoint f x); [easy | apply seq_lim_lim].
Qed.
End BanachFixpoint.
QArith
stdlib_rationals Qinf Qpossec QposInf QnonNeg abstract_algebra QType_rationals additional_operations.
Require Import Qauto QOrderedType.
Require Import theory.rings theory.dec_fields orders.rings orders.dec_fields nat_pow.
Require Import interfaces.naturals interfaces.orders.
Import peano_naturals.
Require Import CRGeometricSum.
Import Qround Qpower.
Require Import metric.
Local Notation ball := mspc_ball.
Local Notation "x ²" := (x × x) (at level 30) : mc_scope.
Section BanachFixpoint.
Add Field Q : (stdlib_field_theory Q).
Context `{MetricSpaceClass X} {Xlim : Limit X} {Xcms : CompleteMetricSpaceClass X}.
Context (f : X → X) `{!IsContraction f q} (x0 : X).
Let x n := nat_iter n f x0.
Arguments x n%mc.
Lemma x_Sn : ∀ n, x (1 + n) = f (x n).
Proof. reflexivity. Qed.
Let d := msd (x 0) (x 1).
Instance : PropHolds (0 ≤ d).
Proof. apply msd_nonneg. Qed.
Instance : PropHolds (0 ≤ q).
Proof. apply (lip_nonneg f q).
Qed.
Instance : PropHolds (q < 1).
Proof. apply (contr_lt_1 f q). Qed.
Instance : PropHolds (0 < 1 - q).
Proof.
assert (A := contr_lt_1 f q).
rewrite <- flip_lt_negate in A. apply (strictly_order_preserving (1 +)) in A.
now rewrite plus_negate_r in A.
Qed.
Global Instance : ∀ q : Q, PropHolds (0 < q) → PropHolds (q ≠ 0).
Proof. apply lt_ne_flip. Qed.
Lemma dist_xn_xSn : ∀ n : nat, ball (d × q^n) (x n) (x (1 + n)).
Proof.
induction n using nat_induction.
+ rewrite nat_pow_0, right_identity; subst d; apply mspc_distance.
+ rewrite nat_pow_S. mc_setoid_replace (d × (q × q ^ n)) with (q × (d × q^n)) by ring.
change (x (1 + n)) with (f (x n)); change (x (1 + (1 + n))) with (f (x (1 + n))).
now apply contr_prf.
Qed.
Lemma dist_xm_xn : ∀ m n : nat, ball (d × q^m × (1 - q^n) / (1 - q)) (x m) (x (m + n)).
Proof.
intro m; induction n as [| n IH] using nat_induction.
+ rewrite right_identity; apply mspc_refl.
now rewrite nat_pow_0, plus_negate_r, right_absorb, left_absorb.
+ apply (mspc_triangle' (d × q^m × (1 - q^n) / (1 - q))%mc (d × q^(m + n))%mc (x (m + n))); trivial.
- rewrite nat_pow_S, nat_pow_exp_plus. field; solve_propholds.
- mc_setoid_replace (m + (1 + n)) with (1 + (m + n)) by ring. apply dist_xn_xSn.
Qed.
Lemma dist_xm_xn' : ∀ m n : nat, ball (d × q^m / (1 - q)) (x m) (x (m + n)).
Proof.
intros m n. apply (mspc_monotone (d × q^m × (1 - q^n) / (1 - q))%mc); [| apply dist_xm_xn].
apply (order_preserving (.* /(1 - q))). rewrite <- associativity.
apply (order_preserving (d *.)). rewrite <- (mult_1_r (q^m)) at 2.
apply (order_preserving (q^m *.)). rewrite <- (plus_0_r 1) at 2.
apply (order_preserving (1 +)). rewrite <- negate_0.
apply flip_le_negate. solve_propholds.
Qed.
Lemma Qpower_mc_power (e : Q) (n : nat) : (e ^ n)%Q = (e ^ n)%mc.
Proof.
induction n as [| n IH] using nat_induction.
+ now rewrite nat_pow_0.
+ rewrite Nat2Z.inj_add, Qpower_plus'.
- now rewrite nat_pow_S, IH.
- rewrite <- Nat2Z.inj_add; change 0%Z with (Z.of_nat 0); rewrite Nat2Z.inj_iff;
apply not_eq_sym, O_S.
Qed.
Lemma Qstepl : ∀ (x y z : Q), x ≤ y → x = z → z ≤ y.
Proof. intros ? ? ? ? A2; now rewrite <- A2. Qed.
Lemma Qstepr : ∀ (x y z : Q), x ≤ y → y = z → x ≤ z.
Proof. intros ? ? ? ? A2; now rewrite <- A2. Qed.
Declare Left Step Qstepl.
Declare Right Step Qstepr.
Lemma binom_ineq (a : Q) (n : nat) : -1 ≤ a → 1 + (n : Q) × a ≤ (1 + a)^n.
Proof.
intro A.
assert (A1 : 0 ≤ 1 + a) by (now apply (order_preserving (1 +)) in A; rewrite plus_negate_r in A).
induction n as [| n IH] using nat_induction.
+ rewrite nat_pow_0; change (1 + 0 × a ≤ 1); now rewrite mult_0_l, plus_0_r.
+ rewrite nat_pow_S. transitivity ((1 + a) × (1 + (n : Q) × a)).
- rewrite Nat2Z.inj_add, inject_Z_plus.
stepr (1 + (1 + (n : Q)) × a + (n : Q) × a²) by ring.
apply nonneg_plus_le_compat_r. apply nonneg_mult_compat; [solve_propholds | apply square_nonneg].
- now apply (order_preserving ((1 + a) *.)) in IH.
Qed.
Lemma nat_pow_recip `{DecField A} `{Naturals B} `{!NatPowSpec A B pw} :
(∀ x y : A, Decision (x = y)) →
∀ (a : A) (n : B), (/a) ^ n = /(a ^ n).
Proof.
intros D a. apply naturals.induction.
+ intros n1 n2 E; now rewrite E.
+ rewrite !nat_pow_0; symmetry; apply dec_recip_1.
+ intros n IH. now rewrite !nat_pow_S, dec_recip_distr, IH.
Qed.
Lemma power_tends_to_zero (e : Q) (n : nat) :
0 < e → Z.to_nat (Qceiling (/(e × (1 - q)))%mc) ≤ n → q ^ n ≤ e.
Proof.
intros A1 A2.
assert (A3 : 0 < n).
+ let T := type of A2 in match T with (?lhs ≤ _) ⇒ apply lt_le_trans with (y := lhs) end; [| trivial].
apply Q.Qlt_lt_of_nat_inject_Z; change (0 < / (e × (1 - q))); solve_propholds.
+ destruct n as [| n]; [elim (lt_irrefl _ A3) |].
rewrite <- Qpower_mc_power.
apply GeometricCovergenceLemma with (e := e ↾ A1); [solve_propholds .. |].
apply (Q.le_Qle_Qceiling_to_nat _ (S n)), A2.
Qed.
Lemma const_x (N : Q → nat) : d = 0 → cauchy x N.
Proof.
intro eq_d_0.
assert (A := mspc_distance (x 0) (x 1)).
subst d; rewrite eq_d_0 in A.
assert (C : ∀ n, x n = x 0).
+ induction n as [| n IH] using nat_induction; [easy |].
change (x (1 + n)) with (f (x n)). rewrite IH. symmetry; apply A.
+ intros e e_pos m n _ _. rewrite (C m), (C n). apply mspc_refl. solve_propholds.
Qed.
Lemma cauchy_x : cauchy x (λ e, Z.to_nat (Qceiling (d / (e × (1 - q)²))%mc)).
Proof.
assert (d_nonneg : 0 ≤ d) by solve_propholds.
assert (d_pos_0 : 0 = d ∨ 0 < d) by now apply le_equiv_lt.
destruct d_pos_0 as [d_0 | d_pos]; [now apply const_x |].
intros e e_pos.
match goal with
|- ∀ m n, @?G m n ⇒ intros m n; assert (A : ∀ m n, m ≤ n → G m n)
end.
+ clear m n; intros m n le_m_n A _.
rewrite <- (cut_minus_le n m); trivial. rewrite plus_comm.
apply (mspc_monotone (d × q^m / (1 - q))%mc); [| apply dist_xm_xn'].
cut (q ^ m ≤ e × (1 - q) / d).
- intro A1. apply (order_preserving (d *.)), (order_preserving (.* /(1 - q))) in A1.
apply (po_proper' A1); [easy | field; split; solve_propholds].
- apply power_tends_to_zero; [solve_propholds |].
apply (po_proper' A); [| easy]. apply f_equal, Qceiling_comp.
match goal with |- (Qeq ?l ?r) ⇒ change (l = r) end.
field; repeat split; solve_propholds.
+ assert (A1 : TotalRelation (A := nat) (≤)) by apply _; destruct (A1 m n).
- now apply A.
- intros; apply mspc_symm; now apply A.
Qed.
Definition fp := lim (reg_fun x _ cauchy_x).
Lemma banach_fixpoint : f fp = fp.
Proof.
assert (C := cauchy_x).
eapply (iter_fixpoint f x); [easy | apply seq_lim_lim].
Qed.
End BanachFixpoint.