Some reshuffling of lemmas

logsem · Oct 11, 2023 · 5eb5b23 · 5eb5b23
1 parent 906c61c
commit 5eb5b23
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 57 deletions.
diff --git a/theories/prelude/Coquelicot_ext.v b/theories/prelude/Coquelicot_ext.v
@@ -181,6 +181,66 @@ Proof.
   apply Rabs_pos.
 Qed.
 
+
+Lemma partial_sum_pos (h : nat → R) p :
+  (∀ n, 0 <= h n) →
+  0 <= sum_n h p.
+Proof.
+  intros Hpos.
+  rewrite /sum_n.
+  induction p.
+  - rewrite sum_n_n; auto.
+  - rewrite sum_n_Sm; auto with arith.
+    apply Rplus_le_le_0_compat; auto.
+Qed.
+
+Lemma partial_sum_elem (h : nat → R) p :
+  (∀ n, 0 <= h n) →
+  h p <= sum_n h p.
+Proof.
+  intros Hpos.
+  rewrite /sum_n.
+  induction p.
+  - rewrite sum_n_n; auto.
+    apply Rle_refl.
+  - rewrite sum_n_Sm; auto with arith.
+    assert (h (S p) = 0 + h (S p)) as Haux; try lra.
+    rewrite {1}Haux.
+    apply Rplus_le_compat; [apply partial_sum_pos | apply Rle_refl]; auto.
+Qed.
+
+Lemma partial_sum_mon (h : nat → R) p q :
+  (∀ n, 0 <= h n) →
+  p ≤ q →
+  sum_n h p <= sum_n h q.
+Proof.
+  intros Hge Hpq.
+  rewrite /sum_n.
+  induction q.
+  - assert (p = 0%nat); auto with arith.
+    simplify_eq; done.
+  - destruct (PeanoNat.Nat.le_gt_cases p q) as [H1 | H1].
+    + specialize (IHq H1).
+      rewrite sum_n_Sm; auto with arith.
+      rewrite /plus /=.
+      specialize (Hge (S q)).
+      lra.
+    + assert (p = S q) as ->; auto with arith.
+      lra.
+Qed.
+
+Lemma sum_n_le (h g: nat → R) n:
+  (∀ m, h m <= g m) →
+  sum_n h n <= sum_n g n.
+Proof.
+  intro Hle.
+  induction n.
+  - rewrite 2!sum_O //.
+  - rewrite 2!sum_Sn.
+    by apply Rplus_le_compat.
+Qed.
+
+
 Lemma is_series_0 a :
   (∀ n, a n = 0) → is_series a 0.
 Proof.

diff --git a/theories/prelude/Series_ext.v b/theories/prelude/Series_ext.v
@@ -39,52 +39,6 @@ Proof.
       apply not_le; auto.
 Qed.
 
-Lemma partial_sum_pos (h : nat → R) p :
-  (∀ n, 0 <= h n) →
-  0 <= sum_n h p.
-Proof.
-  intros Hpos.
-  rewrite /sum_n.
-  induction p.
-  - rewrite sum_n_n; auto.
-  - rewrite sum_n_Sm; auto with arith.
-    apply Rplus_le_le_0_compat; auto.
-Qed.
-
-Lemma partial_sum_elem (h : nat → R) p :
-  (∀ n, 0 <= h n) →
-  h p <= sum_n h p.
-Proof.
-  intros Hpos.
-  rewrite /sum_n.
-  induction p.
-  - rewrite sum_n_n; auto.
-    apply Rle_refl.
-  - rewrite sum_n_Sm; auto with arith.
-    assert (h (S p) = 0 + h (S p)) as Haux; try lra.
-    rewrite {1}Haux.
-    apply Rplus_le_compat; [apply partial_sum_pos | apply Rle_refl]; auto.
-Qed.
-
-Lemma partial_sum_mon (h : nat → R) p q :
-  (∀ n, 0 <= h n) →
-  p ≤ q →
-  sum_n h p <= sum_n h q.
-Proof.
-  intros Hge Hpq.
-  rewrite /sum_n.
-  induction q.
-  - assert (p = 0%nat); auto with arith.
-    simplify_eq; done.
-  - destruct (PeanoNat.Nat.le_gt_cases p q) as [H1 | H1].
-    + specialize (IHq H1).
-      rewrite sum_n_Sm; auto with arith.
-      rewrite /plus /=.
-      specialize (Hge (S q)).
-      lra.
-    + assert (p = S q) as ->; auto with arith.
-      lra.
-Qed.
 
 Lemma is_series_ge0 (h : nat → R) r:
   (∀ n, 0 <= h n) →
@@ -468,17 +422,6 @@ Lemma fubini_fin_sum (h : nat * nat → R) n m:
   = sum_n (λ b, sum_n (λ a, h (a, b)) m ) n.
 Proof. intros. apply sum_n_switch. Qed.
 
-Lemma sum_n_le (h g: nat → R) n:
-  (∀ m, h m <= g m) →
-  sum_n h n <= sum_n g n.
-Proof.
-  intro Hle.
-  induction n.
-  - rewrite 2!sum_O //.
-  - rewrite 2!sum_Sn.
-    by apply Rplus_le_compat.
-Qed.
-
 Lemma series_pos_partial_le (h : nat → R) n:
   (∀ a, 0 <= h a) →
   ex_series h →