-
Notifications
You must be signed in to change notification settings - Fork 0
/
Harmonic.v
105 lines (81 loc) · 2.72 KB
/
Harmonic.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
Require Import Summing.
Require Import Coq.Reals.Reals.
Require Import Omega.
Require Nat.
Local Open Scope R_scope.
(* divergence of harmonic series *)
Definition harmonic (n:nat) := /(INR (S n)).
(* General result about decomposing a sum in chunks *)
Definition chunk_sums u (n:nat):= sum (from u (2^n)) (2^n).
Lemma chunk_decomposition: forall u n, sum u (2^n) = sum (chunk_sums u) n + u O.
Proof.
intros.
induction n as [|n' IHn']; [trivial|].
replace ((2^(S n'))%nat) with ((2^n' + 2^n')%nat) by (rewrite Nat.pow_succ_r; intuition).
replace (sum u (2 ^ n' + 2 ^ n')) with (sum u (2^n') + sum (from u (2^n')) (2^n')) by (auto using sum_sum_from).
rewrite IHn'. simpl. unfold chunk_sums. field.
Qed.
Lemma harm_decr: forall n m, (n <= m)%nat -> harmonic m <= harmonic n.
Proof.
intros. unfold harmonic. apply Rinv_le_contravar; intuition.
Qed.
Lemma pow_INR: forall (x:R) (m:nat),
x = INR m
-> forall n, x^n = INR (m^n).
Proof.
intros x m H n.
induction n as [|n' IHn']; [trivial|].
simpl. rewrite mult_INR. congruence.
Qed.
Lemma half': forall n, (/2 = (2^n) * / 2^(S n)).
Proof.
intros. simpl. field. apply pow_nonzero. discrR.
Qed.
Lemma tech__: forall n, INR (2 * 2 ^ n - 1) + 1 = 2 * 2 ^ n.
Proof.
intros.
replace ((2*2^n)%nat) with ((2^(S n))%nat) by intuition.
assert (2^0 <= 2 ^ S n)%nat.
-
apply Nat.pow_le_mono_r; intuition.
-
rewrite minus_INR; intuition.
replace (INR 1) with 1 by intuition.
replace (2*2^n) with (2^(S n)) by intuition.
rewrite (pow_INR 2 2%nat). field. intuition.
Qed.
Lemma tech_: forall n, harmonic (2 ^ n + 2 ^ n - 1) = / 2 ^ S n.
Proof.
intros.
unfold harmonic.
simpl (2^(S n)).
replace (2 ^ n + 2 ^ n)%nat with (2* 2 ^ n)%nat by omega.
assert (INR (S (2 * 2 ^ n - 1)) = 2 * 2 ^ n); intuition.
rewrite S_INR. apply tech__.
Qed.
Lemma harmonic_chunk_ge_half: forall n, /2 <= chunk_sums harmonic n.
Proof.
intros n.
rewrite (half' n).
rewrite (pow_INR 2 2%nat); [|trivial].
rewrite <- tech_.
replace (harmonic (2 ^ n + 2 ^ n - 1)) with (from harmonic (2^n) (2^n - 1)) by (unfold from; intuition).
apply lbound_decr.
unfold from. intros. apply harm_decr. intuition.
Qed.
Lemma sum_harm': forall n, sum (fun k => /2) n + 1 <= sum harmonic (2^n).
Proof.
intros.
rewrite chunk_decomposition.
assert (sum (fun _ : nat => / 2) n <= sum (chunk_sums harmonic) n ).
apply sum_le. apply harmonic_chunk_ge_half.
replace (harmonic 0) with 1; intuition.
Qed.
Theorem sum_harm: forall n, (INR n)/2 +1 <= sum harmonic (2^n).
Proof.
intros.
replace (INR n / 2) with (INR n * /2) by intuition.
replace (INR n * /2) with (sum (from (fun k => /2) 0) n).
- apply sum_harm'.
- refine (sum_const _ _).
Qed.