Skip to content

Commit ac54453

Browse files
lowasserlowasser
authored
The harmonic series diverges (#1708)
Completes #1700, the 34th of the 100 Theorems. Builds on #1707.
1 parent 446ef79 commit ac54453

27 files changed

+716
-110
lines changed

‎src/analysis/convergent-series-metric-abelian-groups.lagda.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ module _
4343
is-sum-prop-series-Metric-Ab =
4444
is-limit-prop-sequence-Metric-Space
4545
( metric-space-Metric-Ab G)
46-
( partial-sum-series-Metric-Ab G σ)
46+
( partial-sum-series-Metric-Ab σ)
4747
4848
is-sum-series-Metric-Ab : type-Metric-Ab G → UU l2
4949
is-sum-series-Metric-Ab s = type-Prop (is-sum-prop-series-Metric-Ab s)
@@ -52,7 +52,7 @@ module _
5252
is-convergent-prop-series-Metric-Ab =
5353
subtype-convergent-sequence-Metric-Space
5454
( metric-space-Metric-Ab G)
55-
( partial-sum-series-Metric-Ab G σ)
55+
( partial-sum-series-Metric-Ab σ)
5656
5757
is-convergent-series-Metric-Ab : UU (l1 ⊔ l2)
5858
is-convergent-series-Metric-Ab =
@@ -76,7 +76,7 @@ module _
7676
7777
partial-sum-convergent-series-Metric-Ab : sequence (type-Metric-Ab G)
7878
partial-sum-convergent-series-Metric-Ab =
79-
partial-sum-series-Metric-Ab G series-convergent-series-Metric-Ab
79+
partial-sum-series-Metric-Ab series-convergent-series-Metric-Ab
8080
```
8181

8282
## The partial sums of a convergent series have a limit, the sum of the series

‎src/analysis/series-metric-abelian-groups.lagda.md‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ module _
8383

8484
```agda
8585
module _
86-
{l1 l2 : Level} (G : Metric-Ab l1 l2)
86+
{l1 l2 : Level} {G : Metric-Ab l1 l2}
8787
where
8888
8989
partial-sum-series-Metric-Ab : series-Metric-Ab G → ℕ → type-Metric-Ab G
@@ -95,14 +95,14 @@ module _
9595

9696
```agda
9797
module _
98-
{l1 l2 : Level} (G : Metric-Ab l1 l2)
98+
{l1 l2 : Level} {G : Metric-Ab l1 l2}
9999
where
100100
101101
eq-term-diff-partial-sum-series-Metric-Ab :
102102
(f : series-Metric-Ab G) (n : ℕ) →
103103
add-Metric-Ab G
104-
( partial-sum-series-Metric-Ab G f (succ-ℕ n))
105-
( neg-Metric-Ab G (partial-sum-series-Metric-Ab G f n)) ＝
104+
( partial-sum-series-Metric-Ab f (succ-ℕ n))
105+
( neg-Metric-Ab G (partial-sum-series-Metric-Ab f n)) ＝
106106
term-series-Metric-Ab f n
107107
eq-term-diff-partial-sum-series-Metric-Ab (series-terms-Metric-Ab f) n =
108108
ap-add-Metric-Ab G
@@ -118,21 +118,21 @@ module _
118118

119119
```agda
120120
module _
121-
{l1 l2 : Level} (G : Metric-Ab l1 l2)
121+
{l1 l2 : Level} {G : Metric-Ab l1 l2}
122122
where
123123
124124
htpy-htpy-partial-sum-series-Metric-Ab :
125125
{σ τ : series-Metric-Ab G} →
126-
(partial-sum-series-Metric-Ab G σ ~ partial-sum-series-Metric-Ab G τ) →
126+
(partial-sum-series-Metric-Ab σ ~ partial-sum-series-Metric-Ab τ) →
127127
term-series-Metric-Ab σ ~ term-series-Metric-Ab τ
128128
htpy-htpy-partial-sum-series-Metric-Ab {σ} {τ} psσ~psτ n =
129-
inv (eq-term-diff-partial-sum-series-Metric-Ab G σ n) ∙
129+
inv (eq-term-diff-partial-sum-series-Metric-Ab σ n) ∙
130130
ap-right-subtraction-Ab (ab-Metric-Ab G) (psσ~psτ (succ-ℕ n)) (psσ~psτ n) ∙
131-
eq-term-diff-partial-sum-series-Metric-Ab G τ n
131+
eq-term-diff-partial-sum-series-Metric-Ab τ n
132132
133133
eq-htpy-partial-sum-series-Metric-Ab :
134134
{σ τ : series-Metric-Ab G} →
135-
(partial-sum-series-Metric-Ab G σ ~ partial-sum-series-Metric-Ab G τ) →
135+
(partial-sum-series-Metric-Ab σ ~ partial-sum-series-Metric-Ab τ) →
136136
σ ＝ τ
137137
eq-htpy-partial-sum-series-Metric-Ab psσ~psτ =
138138
eq-htpy-term-series-Metric-Ab G
@@ -155,31 +155,30 @@ module _
155155

156156
```agda
157157
module _
158-
{l1 l2 : Level} (G : Metric-Ab l1 l2)
158+
{l1 l2 : Level} {G : Metric-Ab l1 l2}
159159
where
160160
161161
abstract
162162
partial-sum-drop-series-Metric-Ab :
163-
(n : ℕ) → (σ : series-Metric-Ab G) → (i : ℕ) →
164-
partial-sum-series-Metric-Ab G (drop-series-Metric-Ab n σ) i ＝
163+
(n : ℕ) (σ : series-Metric-Ab G) (i : ℕ) →
164+
partial-sum-series-Metric-Ab (drop-series-Metric-Ab n σ) i ＝
165165
diff-Metric-Ab G
166-
( partial-sum-series-Metric-Ab G σ (n +ℕ i))
167-
( partial-sum-series-Metric-Ab G σ n)
168-
partial-sum-drop-series-Metric-Ab n (series-terms-Metric-Ab σ) i =
166+
( partial-sum-series-Metric-Ab σ (n +ℕ i))
167+
( partial-sum-series-Metric-Ab σ n)
168+
partial-sum-drop-series-Metric-Ab n s@(series-terms-Metric-Ab σ) i =
169169
inv
170170
( equational-reasoning
171171
diff-Metric-Ab G
172-
( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ)
173-
( n +ℕ i))
174-
( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n)
172+
( partial-sum-series-Metric-Ab s (n +ℕ i))
173+
( partial-sum-series-Metric-Ab s n)
175174
＝
176175
diff-Metric-Ab G
177176
( add-Metric-Ab G
178177
( sum-fin-sequence-type-Ab (ab-Metric-Ab G) n
179178
( σ ∘ nat-Fin (n +ℕ i) ∘ inl-coproduct-Fin n i))
180179
( sum-fin-sequence-type-Ab (ab-Metric-Ab G) i
181180
( σ ∘ nat-Fin (n +ℕ i) ∘ inr-coproduct-Fin n i)))
182-
( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n)
181+
( partial-sum-series-Metric-Ab s n)
183182
by
184183
ap-diff-Metric-Ab G
185184
( split-sum-fin-sequence-type-Ab
@@ -191,10 +190,11 @@ module _
191190
＝
192191
diff-Metric-Ab G
193192
( add-Metric-Ab G
194-
( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n)
195-
( partial-sum-series-Metric-Ab G
196-
( series-terms-Metric-Ab (σ ∘ add-ℕ n)) i))
197-
( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n)
193+
( partial-sum-series-Metric-Ab s n)
194+
( partial-sum-series-Metric-Ab
195+
( series-terms-Metric-Ab {G = G} (σ ∘ add-ℕ n))
196+
( i)))
197+
( partial-sum-series-Metric-Ab s n)
198198
by
199199
ap-diff-Metric-Ab G
200200
( ap-add-Metric-Ab G
@@ -204,8 +204,8 @@ module _
204204
( λ j → ap σ (nat-inr-coproduct-Fin n i j))))
205205
( refl)
206206
＝
207-
partial-sum-series-Metric-Ab G
208-
( series-terms-Metric-Ab (σ ∘ add-ℕ n))
207+
partial-sum-series-Metric-Ab
208+
( series-terms-Metric-Ab {G = G} (σ ∘ add-ℕ n))
209209
( i)
210210
by is-identity-left-conjugation-Ab (ab-Metric-Ab G) _ _)
211211
```

‎src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ module commutative-algebra.sums-of-finite-sequences-of-elements-commutative-ring
88

99
```agda
1010
open import commutative-algebra.commutative-rings
11+
open import commutative-algebra.multiples-of-elements-commutative-rings
1112
1213
open import elementary-number-theory.addition-natural-numbers
1314
open import elementary-number-theory.natural-numbers
@@ -244,6 +245,19 @@ module _
244245
preserves-sum-permutation-fin-sequence-type-Ring (ring-Commutative-Ring A)
245246
```
246247

248+
### The sum of a constant finite sequence in a commutative ring is scalar multiplication by the length of the sequence
249+
250+
```agda
251+
abstract
252+
sum-constant-fin-sequence-type-Commutative-Ring :
253+
{l : Level} (R : Commutative-Ring l) (n : ℕ) →
254+
(x : type-Commutative-Ring R) →
255+
sum-fin-sequence-type-Commutative-Ring R n (λ _ → x) ＝
256+
multiple-Commutative-Ring R n x
257+
sum-constant-fin-sequence-type-Commutative-Ring R =
258+
sum-constant-fin-sequence-type-Ring (ring-Commutative-Ring R)
259+
```
260+
247261
## See also
248262

249263
- [Sums of finite families of elements in commutative rings](commutative-algebra.sums-of-finite-families-of-elements-commutative-rings.md)

‎src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ module commutative-algebra.sums-of-finite-sequences-of-elements-commutative-semi
88

99
```agda
1010
open import commutative-algebra.commutative-semirings
11+
open import commutative-algebra.multiples-of-elements-commutative-semirings
1112
1213
open import elementary-number-theory.addition-natural-numbers
1314
open import elementary-number-theory.natural-numbers
@@ -260,3 +261,16 @@ module _
260261
preserves-sum-permutation-fin-sequence-type-Semiring
261262
( semiring-Commutative-Semiring R)
262263
```
264+
265+
### The sum of a constant finite sequence in a commutative semiring is scalar multiplication by the length of the sequence
266+
267+
```agda
268+
abstract
269+
sum-constant-fin-sequence-type-Commutative-Semiring :
270+
{l : Level} (R : Commutative-Semiring l) (n : ℕ) →
271+
(x : type-Commutative-Semiring R) →
272+
sum-fin-sequence-type-Commutative-Semiring R n (λ _ → x) ＝
273+
multiple-Commutative-Semiring R n x
274+
sum-constant-fin-sequence-type-Commutative-Semiring R =
275+
sum-constant-fin-sequence-type-Semiring (semiring-Commutative-Semiring R)
276+
```

‎src/domain-theory/kleenes-fixed-point-theorem-posets.lagda.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ open import foundation.universe-levels
2626
2727
open import order-theory.bottom-elements-posets
2828
open import order-theory.chains-posets
29+
open import order-theory.increasing-sequences-posets
2930
open import order-theory.inflattices
3031
open import order-theory.inhabited-chains-posets
3132
open import order-theory.least-upper-bounds-posets

‎src/domain-theory/omega-continuous-maps-omega-complete-posets.lagda.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ open import foundation.surjective-maps
3434
open import foundation.torsorial-type-families
3535
open import foundation.universe-levels
3636
37+
open import order-theory.increasing-sequences-posets
3738
open import order-theory.join-preserving-maps-posets
3839
open import order-theory.least-upper-bounds-posets
3940
open import order-theory.order-preserving-maps-posets

‎src/domain-theory/omega-continuous-maps-posets.lagda.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ open import foundation.surjective-maps
3232
open import foundation.torsorial-type-families
3333
open import foundation.universe-levels
3434
35+
open import order-theory.increasing-sequences-posets
3536
open import order-theory.join-preserving-maps-posets
3637
open import order-theory.least-upper-bounds-posets
3738
open import order-theory.order-preserving-maps-posets

‎src/elementary-number-theory.lagda.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,7 @@ open import elementary-number-theory.greatest-common-divisor-natural-numbers pub
9292
open import elementary-number-theory.group-of-integers public
9393
open import elementary-number-theory.half-integers public
9494
open import elementary-number-theory.hardy-ramanujan-number public
95+
open import elementary-number-theory.harmonic-series-rational-numbers public
9596
open import elementary-number-theory.inclusion-natural-numbers-conatural-numbers public
9697
open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers public
9798
open import elementary-number-theory.inequality-arithmetic-geometric-means-integers public
@@ -200,6 +201,7 @@ open import elementary-number-theory.ring-extension-rational-numbers-of-rational
200201
open import elementary-number-theory.ring-of-integers public
201202
open import elementary-number-theory.ring-of-rational-numbers public
202203
open import elementary-number-theory.semiring-of-natural-numbers public
204+
open import elementary-number-theory.series-rational-numbers public
203205
open import elementary-number-theory.sieve-of-eratosthenes public
204206
open import elementary-number-theory.square-free-natural-numbers public
205207
open import elementary-number-theory.square-roots-positive-rational-numbers public
@@ -219,6 +221,7 @@ open import elementary-number-theory.strict-inequality-rational-numbers public
219221
open import elementary-number-theory.strict-inequality-standard-finite-types public
220222
open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
221223
open import elementary-number-theory.strong-induction-natural-numbers public
224+
open import elementary-number-theory.sums-of-finite-sequences-of-rational-numbers public
222225
open import elementary-number-theory.sums-of-natural-numbers public
223226
open import elementary-number-theory.sylvesters-sequence public
224227
open import elementary-number-theory.taxicab-numbers public

‎src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md‎

Lines changed: 0 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -48,50 +48,3 @@ pr1 ℕ-Decidable-Total-Order = ℕ-Poset
4848
pr1 (pr2 ℕ-Decidable-Total-Order) = is-total-leq-ℕ
4949
pr2 (pr2 ℕ-Decidable-Total-Order) = is-decidable-leq-ℕ
5050
```
51-
52-
## Properties
53-
54-
### Maps out of the natural numbers that preserve order by induction
55-
56-
```agda
57-
module _
58-
{l1 l2 : Level} (P : Preorder l1 l2)
59-
where
60-
61-
preserves-order-ind-ℕ-Preorder :
62-
(f : ℕ → type-Preorder P) →
63-
((n : ℕ) → leq-Preorder P (f n) (f (succ-ℕ n))) →
64-
preserves-order-Preorder ℕ-Preorder P f
65-
preserves-order-ind-ℕ-Preorder f H zero-ℕ zero-ℕ p =
66-
refl-leq-Preorder P (f zero-ℕ)
67-
preserves-order-ind-ℕ-Preorder f H zero-ℕ (succ-ℕ m) p =
68-
transitive-leq-Preorder P (f 0) (f m) (f (succ-ℕ m))
69-
( H m)
70-
( preserves-order-ind-ℕ-Preorder f H zero-ℕ m star)
71-
preserves-order-ind-ℕ-Preorder f H (succ-ℕ n) zero-ℕ ()
72-
preserves-order-ind-ℕ-Preorder f H (succ-ℕ n) (succ-ℕ m) =
73-
preserves-order-ind-ℕ-Preorder (f ∘ succ-ℕ) (H ∘ succ-ℕ) n m
74-
75-
hom-ind-ℕ-Preorder :
76-
(f : ℕ → type-Preorder P) →
77-
((n : ℕ) → leq-Preorder P (f n) (f (succ-ℕ n))) →
78-
hom-Preorder (ℕ-Preorder) P
79-
hom-ind-ℕ-Preorder f H = f , preserves-order-ind-ℕ-Preorder f H
80-
81-
module _
82-
{l1 l2 : Level} (P : Poset l1 l2)
83-
where
84-
85-
preserves-order-ind-ℕ-Poset :
86-
(f : ℕ → type-Poset P) →
87-
((n : ℕ) → leq-Poset P (f n) (f (succ-ℕ n))) →
88-
preserves-order-Poset ℕ-Poset P f
89-
preserves-order-ind-ℕ-Poset =
90-
preserves-order-ind-ℕ-Preorder (preorder-Poset P)
91-
92-
hom-ind-ℕ-Poset :
93-
(f : ℕ → type-Poset P) →
94-
((n : ℕ) → leq-Poset P (f n) (f (succ-ℕ n))) →
95-
hom-Poset (ℕ-Poset) P
96-
hom-ind-ℕ-Poset = hom-ind-ℕ-Preorder (preorder-Poset P)
97-
```

‎src/elementary-number-theory/exponentiation-natural-numbers.lagda.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,12 @@ open import commutative-algebra.powers-of-elements-commutative-semirings
1212
open import elementary-number-theory.addition-natural-numbers
1313
open import elementary-number-theory.multiplication-natural-numbers
1414
open import elementary-number-theory.natural-numbers
15+
open import elementary-number-theory.nonzero-natural-numbers
1516
open import elementary-number-theory.products-of-natural-numbers
1617
open import elementary-number-theory.semiring-of-natural-numbers
1718
1819
open import foundation.action-on-identifications-functions
20+
open import foundation.dependent-pair-types
1921
open import foundation.identity-types
2022
```
2123

@@ -103,6 +105,9 @@ abstract
103105
is-nonzero-exp-ℕ m zero-ℕ p = is-nonzero-one-ℕ
104106
is-nonzero-exp-ℕ m (succ-ℕ n) p =
105107
is-nonzero-mul-ℕ (m ^ℕ n) m (is-nonzero-exp-ℕ m n p) p
108+
109+
exp-ℕ⁺ : ℕ⁺ → ℕ → ℕ⁺
110+
exp-ℕ⁺ (n , n≠0) m = (exp-ℕ n m , is-nonzero-exp-ℕ n m n≠0)
106111
```
107112

108113
### The exponent $m^n$ is equal to the $n$-fold product of $m$

0 commit comments

Comments
 (0)