diff --git a/src/analysis/convergent-series-metric-abelian-groups.lagda.md b/src/analysis/convergent-series-metric-abelian-groups.lagda.md index 6e5e9cfe3f..d78cf2b8bd 100644 --- a/src/analysis/convergent-series-metric-abelian-groups.lagda.md +++ b/src/analysis/convergent-series-metric-abelian-groups.lagda.md @@ -43,7 +43,7 @@ module _ is-sum-prop-series-Metric-Ab = is-limit-prop-sequence-Metric-Space ( metric-space-Metric-Ab G) - ( partial-sum-series-Metric-Ab G σ) + ( partial-sum-series-Metric-Ab σ) is-sum-series-Metric-Ab : type-Metric-Ab G → UU l2 is-sum-series-Metric-Ab s = type-Prop (is-sum-prop-series-Metric-Ab s) @@ -52,7 +52,7 @@ module _ is-convergent-prop-series-Metric-Ab = subtype-convergent-sequence-Metric-Space ( metric-space-Metric-Ab G) - ( partial-sum-series-Metric-Ab G σ) + ( partial-sum-series-Metric-Ab σ) is-convergent-series-Metric-Ab : UU (l1 ⊔ l2) is-convergent-series-Metric-Ab = @@ -76,7 +76,7 @@ module _ partial-sum-convergent-series-Metric-Ab : sequence (type-Metric-Ab G) partial-sum-convergent-series-Metric-Ab = - partial-sum-series-Metric-Ab G series-convergent-series-Metric-Ab + partial-sum-series-Metric-Ab series-convergent-series-Metric-Ab ``` ## The partial sums of a convergent series have a limit, the sum of the series diff --git a/src/analysis/series-metric-abelian-groups.lagda.md b/src/analysis/series-metric-abelian-groups.lagda.md index 1bb3d80a5e..b450b78d25 100644 --- a/src/analysis/series-metric-abelian-groups.lagda.md +++ b/src/analysis/series-metric-abelian-groups.lagda.md @@ -83,7 +83,7 @@ module _ ```agda module _ - {l1 l2 : Level} (G : Metric-Ab l1 l2) + {l1 l2 : Level} {G : Metric-Ab l1 l2} where partial-sum-series-Metric-Ab : series-Metric-Ab G → ℕ → type-Metric-Ab G @@ -95,14 +95,14 @@ module _ ```agda module _ - {l1 l2 : Level} (G : Metric-Ab l1 l2) + {l1 l2 : Level} {G : Metric-Ab l1 l2} where eq-term-diff-partial-sum-series-Metric-Ab : (f : series-Metric-Ab G) (n : ℕ) → add-Metric-Ab G - ( partial-sum-series-Metric-Ab G f (succ-ℕ n)) - ( neg-Metric-Ab G (partial-sum-series-Metric-Ab G f n)) ＝ + ( partial-sum-series-Metric-Ab f (succ-ℕ n)) + ( neg-Metric-Ab G (partial-sum-series-Metric-Ab f n)) ＝ term-series-Metric-Ab f n eq-term-diff-partial-sum-series-Metric-Ab (series-terms-Metric-Ab f) n = ap-add-Metric-Ab G @@ -118,21 +118,21 @@ module _ ```agda module _ - {l1 l2 : Level} (G : Metric-Ab l1 l2) + {l1 l2 : Level} {G : Metric-Ab l1 l2} where htpy-htpy-partial-sum-series-Metric-Ab : {σ τ : series-Metric-Ab G} → - (partial-sum-series-Metric-Ab G σ ~ partial-sum-series-Metric-Ab G τ) → + (partial-sum-series-Metric-Ab σ ~ partial-sum-series-Metric-Ab τ) → term-series-Metric-Ab σ ~ term-series-Metric-Ab τ htpy-htpy-partial-sum-series-Metric-Ab {σ} {τ} psσ~psτ n = - inv (eq-term-diff-partial-sum-series-Metric-Ab G σ n) ∙ + inv (eq-term-diff-partial-sum-series-Metric-Ab σ n) ∙ ap-right-subtraction-Ab (ab-Metric-Ab G) (psσ~psτ (succ-ℕ n)) (psσ~psτ n) ∙ - eq-term-diff-partial-sum-series-Metric-Ab G τ n + eq-term-diff-partial-sum-series-Metric-Ab τ n eq-htpy-partial-sum-series-Metric-Ab : {σ τ : series-Metric-Ab G} → - (partial-sum-series-Metric-Ab G σ ~ partial-sum-series-Metric-Ab G τ) → + (partial-sum-series-Metric-Ab σ ~ partial-sum-series-Metric-Ab τ) → σ ＝ τ eq-htpy-partial-sum-series-Metric-Ab psσ~psτ = eq-htpy-term-series-Metric-Ab G @@ -155,23 +155,22 @@ module _ ```agda module _ - {l1 l2 : Level} (G : Metric-Ab l1 l2) + {l1 l2 : Level} {G : Metric-Ab l1 l2} where abstract partial-sum-drop-series-Metric-Ab : - (n : ℕ) → (σ : series-Metric-Ab G) → (i : ℕ) → - partial-sum-series-Metric-Ab G (drop-series-Metric-Ab n σ) i ＝ + (n : ℕ) (σ : series-Metric-Ab G) (i : ℕ) → + partial-sum-series-Metric-Ab (drop-series-Metric-Ab n σ) i ＝ diff-Metric-Ab G - ( partial-sum-series-Metric-Ab G σ (n +ℕ i)) - ( partial-sum-series-Metric-Ab G σ n) - partial-sum-drop-series-Metric-Ab n (series-terms-Metric-Ab σ) i = + ( partial-sum-series-Metric-Ab σ (n +ℕ i)) + ( partial-sum-series-Metric-Ab σ n) + partial-sum-drop-series-Metric-Ab n s@(series-terms-Metric-Ab σ) i = inv ( equational-reasoning diff-Metric-Ab G - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) - ( n +ℕ i)) - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n) + ( partial-sum-series-Metric-Ab s (n +ℕ i)) + ( partial-sum-series-Metric-Ab s n) ＝ diff-Metric-Ab G ( add-Metric-Ab G @@ -179,7 +178,7 @@ module _ ( σ ∘ nat-Fin (n +ℕ i) ∘ inl-coproduct-Fin n i)) ( sum-fin-sequence-type-Ab (ab-Metric-Ab G) i ( σ ∘ nat-Fin (n +ℕ i) ∘ inr-coproduct-Fin n i))) - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n) + ( partial-sum-series-Metric-Ab s n) by ap-diff-Metric-Ab G ( split-sum-fin-sequence-type-Ab @@ -191,10 +190,11 @@ module _ ＝ diff-Metric-Ab G ( add-Metric-Ab G - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n) - ( partial-sum-series-Metric-Ab G - ( series-terms-Metric-Ab (σ ∘ add-ℕ n)) i)) - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n) + ( partial-sum-series-Metric-Ab s n) + ( partial-sum-series-Metric-Ab + ( series-terms-Metric-Ab {G = G} (σ ∘ add-ℕ n)) + ( i))) + ( partial-sum-series-Metric-Ab s n) by ap-diff-Metric-Ab G ( ap-add-Metric-Ab G @@ -204,8 +204,8 @@ module _ ( λ j → ap σ (nat-inr-coproduct-Fin n i j)))) ( refl) ＝ - partial-sum-series-Metric-Ab G - ( series-terms-Metric-Ab (σ ∘ add-ℕ n)) + partial-sum-series-Metric-Ab + ( series-terms-Metric-Ab {G = G} (σ ∘ add-ℕ n)) ( i) by is-identity-left-conjugation-Ab (ab-Metric-Ab G) _ _) ``` diff --git a/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md b/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md index b1a0ac28aa..f5113246e1 100644 --- a/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md +++ b/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md @@ -8,6 +8,7 @@ module commutative-algebra.sums-of-finite-sequences-of-elements-commutative-ring ```agda open import commutative-algebra.commutative-rings +open import commutative-algebra.multiples-of-elements-commutative-rings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers @@ -244,6 +245,19 @@ module _ preserves-sum-permutation-fin-sequence-type-Ring (ring-Commutative-Ring A) ``` +### The sum of a constant finite sequence in a commutative ring is scalar multiplication by the length of the sequence + +```agda +abstract + sum-constant-fin-sequence-type-Commutative-Ring : + {l : Level} (R : Commutative-Ring l) (n : ℕ) → + (x : type-Commutative-Ring R) → + sum-fin-sequence-type-Commutative-Ring R n (λ _ → x) ＝ + multiple-Commutative-Ring R n x + sum-constant-fin-sequence-type-Commutative-Ring R = + sum-constant-fin-sequence-type-Ring (ring-Commutative-Ring R) +``` + ## See also - [Sums of finite families of elements in commutative rings](commutative-algebra.sums-of-finite-families-of-elements-commutative-rings.md) diff --git a/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md b/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md index 5c5bfabafc..4292c3ed0e 100644 --- a/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md +++ b/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md @@ -8,6 +8,7 @@ module commutative-algebra.sums-of-finite-sequences-of-elements-commutative-semi ```agda open import commutative-algebra.commutative-semirings +open import commutative-algebra.multiples-of-elements-commutative-semirings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers @@ -260,3 +261,16 @@ module _ preserves-sum-permutation-fin-sequence-type-Semiring ( semiring-Commutative-Semiring R) ``` + +### The sum of a constant finite sequence in a commutative semiring is scalar multiplication by the length of the sequence + +```agda +abstract + sum-constant-fin-sequence-type-Commutative-Semiring : + {l : Level} (R : Commutative-Semiring l) (n : ℕ) → + (x : type-Commutative-Semiring R) → + sum-fin-sequence-type-Commutative-Semiring R n (λ _ → x) ＝ + multiple-Commutative-Semiring R n x + sum-constant-fin-sequence-type-Commutative-Semiring R = + sum-constant-fin-sequence-type-Semiring (semiring-Commutative-Semiring R) +``` diff --git a/src/domain-theory/kleenes-fixed-point-theorem-posets.lagda.md b/src/domain-theory/kleenes-fixed-point-theorem-posets.lagda.md index 8a3518c188..a3adf12194 100644 --- a/src/domain-theory/kleenes-fixed-point-theorem-posets.lagda.md +++ b/src/domain-theory/kleenes-fixed-point-theorem-posets.lagda.md @@ -26,6 +26,7 @@ open import foundation.universe-levels open import order-theory.bottom-elements-posets open import order-theory.chains-posets +open import order-theory.increasing-sequences-posets open import order-theory.inflattices open import order-theory.inhabited-chains-posets open import order-theory.least-upper-bounds-posets diff --git a/src/domain-theory/omega-continuous-maps-omega-complete-posets.lagda.md b/src/domain-theory/omega-continuous-maps-omega-complete-posets.lagda.md index 60ce16827f..cd6d068f2f 100644 --- a/src/domain-theory/omega-continuous-maps-omega-complete-posets.lagda.md +++ b/src/domain-theory/omega-continuous-maps-omega-complete-posets.lagda.md @@ -34,6 +34,7 @@ open import foundation.surjective-maps open import foundation.torsorial-type-families open import foundation.universe-levels +open import order-theory.increasing-sequences-posets open import order-theory.join-preserving-maps-posets open import order-theory.least-upper-bounds-posets open import order-theory.order-preserving-maps-posets diff --git a/src/domain-theory/omega-continuous-maps-posets.lagda.md b/src/domain-theory/omega-continuous-maps-posets.lagda.md index 3781ac426b..8d39239d6e 100644 --- a/src/domain-theory/omega-continuous-maps-posets.lagda.md +++ b/src/domain-theory/omega-continuous-maps-posets.lagda.md @@ -32,6 +32,7 @@ open import foundation.surjective-maps open import foundation.torsorial-type-families open import foundation.universe-levels +open import order-theory.increasing-sequences-posets open import order-theory.join-preserving-maps-posets open import order-theory.least-upper-bounds-posets open import order-theory.order-preserving-maps-posets diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 9177a7585e..33be5ca7f1 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -92,6 +92,7 @@ open import elementary-number-theory.greatest-common-divisor-natural-numbers pub open import elementary-number-theory.group-of-integers public open import elementary-number-theory.half-integers public open import elementary-number-theory.hardy-ramanujan-number public +open import elementary-number-theory.harmonic-series-rational-numbers public open import elementary-number-theory.inclusion-natural-numbers-conatural-numbers public open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers public 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 open import elementary-number-theory.ring-of-integers public open import elementary-number-theory.ring-of-rational-numbers public open import elementary-number-theory.semiring-of-natural-numbers public +open import elementary-number-theory.series-rational-numbers public open import elementary-number-theory.sieve-of-eratosthenes public open import elementary-number-theory.square-free-natural-numbers public 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 open import elementary-number-theory.strict-inequality-standard-finite-types public open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public open import elementary-number-theory.strong-induction-natural-numbers public +open import elementary-number-theory.sums-of-finite-sequences-of-rational-numbers public open import elementary-number-theory.sums-of-natural-numbers public open import elementary-number-theory.sylvesters-sequence public open import elementary-number-theory.taxicab-numbers public diff --git a/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md b/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md index ba6c9d2db7..0317a9a1a3 100644 --- a/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md +++ b/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md @@ -48,50 +48,3 @@ pr1 ℕ-Decidable-Total-Order = ℕ-Poset pr1 (pr2 ℕ-Decidable-Total-Order) = is-total-leq-ℕ pr2 (pr2 ℕ-Decidable-Total-Order) = is-decidable-leq-ℕ ``` - -## Properties - -### Maps out of the natural numbers that preserve order by induction - -```agda -module _ - {l1 l2 : Level} (P : Preorder l1 l2) - where - - preserves-order-ind-ℕ-Preorder : - (f : ℕ → type-Preorder P) → - ((n : ℕ) → leq-Preorder P (f n) (f (succ-ℕ n))) → - preserves-order-Preorder ℕ-Preorder P f - preserves-order-ind-ℕ-Preorder f H zero-ℕ zero-ℕ p = - refl-leq-Preorder P (f zero-ℕ) - preserves-order-ind-ℕ-Preorder f H zero-ℕ (succ-ℕ m) p = - transitive-leq-Preorder P (f 0) (f m) (f (succ-ℕ m)) - ( H m) - ( preserves-order-ind-ℕ-Preorder f H zero-ℕ m star) - preserves-order-ind-ℕ-Preorder f H (succ-ℕ n) zero-ℕ () - preserves-order-ind-ℕ-Preorder f H (succ-ℕ n) (succ-ℕ m) = - preserves-order-ind-ℕ-Preorder (f ∘ succ-ℕ) (H ∘ succ-ℕ) n m - - hom-ind-ℕ-Preorder : - (f : ℕ → type-Preorder P) → - ((n : ℕ) → leq-Preorder P (f n) (f (succ-ℕ n))) → - hom-Preorder (ℕ-Preorder) P - hom-ind-ℕ-Preorder f H = f , preserves-order-ind-ℕ-Preorder f H - -module _ - {l1 l2 : Level} (P : Poset l1 l2) - where - - preserves-order-ind-ℕ-Poset : - (f : ℕ → type-Poset P) → - ((n : ℕ) → leq-Poset P (f n) (f (succ-ℕ n))) → - preserves-order-Poset ℕ-Poset P f - preserves-order-ind-ℕ-Poset = - preserves-order-ind-ℕ-Preorder (preorder-Poset P) - - hom-ind-ℕ-Poset : - (f : ℕ → type-Poset P) → - ((n : ℕ) → leq-Poset P (f n) (f (succ-ℕ n))) → - hom-Poset (ℕ-Poset) P - hom-ind-ℕ-Poset = hom-ind-ℕ-Preorder (preorder-Poset P) -``` diff --git a/src/elementary-number-theory/exponentiation-natural-numbers.lagda.md b/src/elementary-number-theory/exponentiation-natural-numbers.lagda.md index 3e80e5f0dd..acd2ee98f3 100644 --- a/src/elementary-number-theory/exponentiation-natural-numbers.lagda.md +++ b/src/elementary-number-theory/exponentiation-natural-numbers.lagda.md @@ -12,10 +12,12 @@ open import commutative-algebra.powers-of-elements-commutative-semirings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.products-of-natural-numbers open import elementary-number-theory.semiring-of-natural-numbers open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types open import foundation.identity-types ``` @@ -103,6 +105,9 @@ abstract is-nonzero-exp-ℕ m zero-ℕ p = is-nonzero-one-ℕ is-nonzero-exp-ℕ m (succ-ℕ n) p = is-nonzero-mul-ℕ (m ^ℕ n) m (is-nonzero-exp-ℕ m n p) p + +exp-ℕ⁺ : ℕ⁺ → ℕ → ℕ⁺ +exp-ℕ⁺ (n , n≠0) m = (exp-ℕ n m , is-nonzero-exp-ℕ n m n≠0) ``` ### The exponent $m^n$ is equal to the $n$-fold product of $m$ diff --git a/src/elementary-number-theory/harmonic-series-rational-numbers.lagda.md b/src/elementary-number-theory/harmonic-series-rational-numbers.lagda.md new file mode 100644 index 0000000000..87cb5fa105 --- /dev/null +++ b/src/elementary-number-theory/harmonic-series-rational-numbers.lagda.md @@ -0,0 +1,297 @@ +# The harmonic series of rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.harmonic-series-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.addition-nonnegative-rational-numbers +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers +open import elementary-number-theory.archimedean-property-rational-numbers +open import elementary-number-theory.exponentiation-natural-numbers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.positive-and-negative-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.series-rational-numbers +open import elementary-number-theory.strict-inequality-natural-numbers +open import elementary-number-theory.strict-inequality-rational-numbers +open import elementary-number-theory.sums-of-finite-sequences-of-rational-numbers +open import elementary-number-theory.unit-fractions-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.transport-along-identifications + +open import group-theory.abelian-groups + +open import order-theory.posets + +open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +The +{{#concept "harmonic series" WDID=Q464100 WD="harmonic series" Agda=harmonic-series-ℚ}} +is the sum $$∑_{n=0}^{∞} \frac{1}{n}.$$ + +## Definition + +```agda +harmonic-series-ℚ : series-ℚ +harmonic-series-ℚ = series-terms-ℚ reciprocal-rational-succ-ℕ +``` + +## Properties + +### For any `k`, the `2ᵏ`'th partial sum of the harmonic series is at least `1 + k/2` + +```agda +abstract + lower-bound-sum-harmonic-series-power-of-two-ℚ : + (k : ℕ) → + leq-ℚ + ( one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ rational-ℕ k) + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 k)) + lower-bound-sum-harmonic-series-power-of-two-ℚ 0 = + leq-eq-ℚ + ( inv + ( equational-reasoning + partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 zero-ℕ) + ＝ reciprocal-rational-succ-ℕ 0 + by compute-sum-one-element-ℚ _ + ＝ one-ℚ + by ap rational-ℚ⁺ inv-one-ℚ⁺ + ＝ one-ℚ +ℚ zero-ℚ + by inv (right-unit-law-add-ℚ one-ℚ) + ＝ one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ zero-ℚ + by ap-add-ℚ refl (inv (right-zero-law-mul-ℚ _)))) + lower-bound-sum-harmonic-series-power-of-two-ℚ (succ-ℕ n) = + let + open inequality-reasoning-Poset ℚ-Poset + in + chain-of-inequalities + one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ rational-ℕ (succ-ℕ n) + ≤ one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ succ-ℚ (rational-ℕ n) + by leq-eq-ℚ (ap-add-ℚ refl (ap-mul-ℚ refl (inv (succ-rational-ℕ n)))) + ≤ ( one-ℚ) +ℚ + ( reciprocal-rational-succ-ℕ 1 +ℚ + reciprocal-rational-succ-ℕ 1 *ℚ rational-ℕ n) + by leq-eq-ℚ (ap-add-ℚ refl (mul-right-succ-ℚ _ _)) + ≤ ( reciprocal-rational-succ-ℕ 1) +ℚ + ( one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ rational-ℕ n) + by leq-eq-ℚ (left-swap-add-ℚ _ _ _) + ≤ ( reciprocal-rational-succ-ℕ 1) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by + preserves-leq-right-add-ℚ _ _ _ + ( lower-bound-sum-harmonic-series-power-of-two-ℚ n) + ≤ ( ( rational-ℕ (exp-ℕ 2 n)) *ℚ + ( reciprocal-rational-succ-ℕ 1) *ℚ + ( reciprocal-rational-ℕ⁺ (exp-ℕ⁺ two-ℕ⁺ n))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by + leq-eq-ℚ + ( ap-add-ℚ + ( inv + ( ap + ( rational-ℚ⁺) + ( is-identity-left-conjugation-Ab + ( abelian-group-mul-ℚ⁺) + ( positive-rational-ℕ⁺ (exp-ℕ⁺ two-ℕ⁺ n)) + ( positive-reciprocal-rational-succ-ℕ 1)))) + ( refl)) + ≤ ( ( rational-ℕ (exp-ℕ 2 n)) *ℚ + ( ( reciprocal-rational-succ-ℕ 1) *ℚ + ( reciprocal-rational-ℕ⁺ (exp-ℕ⁺ two-ℕ⁺ n)))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by leq-eq-ℚ (ap-add-ℚ (associative-mul-ℚ _ _ _) refl) + ≤ ( ( rational-ℕ (exp-ℕ 2 n)) *ℚ + ( ( reciprocal-rational-ℕ⁺ (exp-ℕ⁺ two-ℕ⁺ n)) *ℚ + ( reciprocal-rational-succ-ℕ 1))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by leq-eq-ℚ (ap-add-ℚ (ap-mul-ℚ refl (commutative-mul-ℚ _ _)) refl) + ≤ ( ( rational-ℕ (exp-ℕ 2 n)) *ℚ + ( reciprocal-rational-ℕ⁺ (exp-ℕ⁺ two-ℕ⁺ (succ-ℕ n)))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by + leq-eq-ℚ + ( ap-add-ℚ + ( ap-mul-ℚ + ( refl) + ( ( inv + ( distributive-reciprocal-mul-ℕ⁺ + ( exp-ℕ⁺ two-ℕ⁺ n) + ( two-ℕ⁺))) ∙ + ( ap + ( reciprocal-rational-ℕ⁺) + ( eq-nonzero-ℕ + { exp-ℕ⁺ two-ℕ⁺ n *ℕ⁺ two-ℕ⁺} + { exp-ℕ⁺ two-ℕ⁺ (succ-ℕ n)} + ( refl))))) + ( refl)) + ≤ ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ _ → reciprocal-rational-ℕ⁺ (exp-ℕ⁺ two-ℕ⁺ (succ-ℕ n)))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by leq-eq-ℚ (ap-add-ℚ (inv (sum-constant-fin-sequence-ℚ _ _)) refl) + ≤ ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inr-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) +ℚ + ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → reciprocal-rational-succ-ℕ (nat-Fin (exp-ℕ 2 n) k))) + by + preserves-leq-left-add-ℚ _ _ _ + ( preserves-leq-sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( _) + ( _) + ( λ k → + inv-leq-ℚ⁺ _ _ + ( preserves-leq-rational-ℕ + ( leq-succ-le-ℕ + ( nat-Fin (exp-ℕ 2 n +ℕ exp-ℕ 2 n) _) + ( exp-ℕ 2 (succ-ℕ n)) + ( inv-tr + ( le-ℕ _) + ( right-two-law-mul-ℕ _) + ( strict-upper-bound-nat-Fin _ _)))))) + ≤ ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inr-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) +ℚ + ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inl-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) + by + leq-eq-ℚ + ( ap-add-ℚ + ( refl) + ( ap + ( sum-fin-sequence-ℚ (exp-ℕ 2 n)) + ( eq-htpy + ( λ k → + ap + ( reciprocal-rational-succ-ℕ) + ( inv (nat-inl-coproduct-Fin _ _ k)))))) + ≤ ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inl-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) +ℚ + ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inr-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) + by leq-eq-ℚ (commutative-add-ℚ _ _) + ≤ sum-fin-sequence-ℚ + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ (nat-Fin (exp-ℕ 2 n +ℕ exp-ℕ 2 n) k)) + by leq-eq-ℚ (inv (split-sum-fin-sequence-ℚ _ _ _)) + ≤ sum-fin-sequence-ℚ + ( exp-ℕ 2 (succ-ℕ n)) + ( reciprocal-rational-succ-ℕ ∘ nat-Fin (exp-ℕ 2 (succ-ℕ n))) + by + leq-eq-ℚ + ( ap + ( λ k → + sum-fin-sequence-ℚ k (reciprocal-rational-succ-ℕ ∘ nat-Fin k)) + ( inv (right-two-law-mul-ℕ _))) +``` + +### The harmonic series diverges + +The divergence of the harmonic series is the +[34th](literature.100-theorems.md#34) theorem on +[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of +[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. + +```agda +abstract + grows-without-bound-harmonic-series-ℚ : + grows-without-bound-series-ℚ harmonic-series-ℚ + grows-without-bound-harmonic-series-ℚ q = + let + open + do-syntax-trunc-Prop + ( ∃ ℕ (partial-sum-stays-above-prop-series-ℚ harmonic-series-ℚ q)) + open inequality-reasoning-Poset ℚ-Poset + in do + (n , 2q @@ -452,17 +455,33 @@ abstract by ap-add-ℚ (right-unit-law-mul-ℚ p) refl ``` +### Multiplication by a natural number is repeated addition + +```agda +abstract + left-mul-rational-nat-ℚ : + (n : ℕ) (q : ℚ) → rational-ℕ n *ℚ q ＝ multiple-Ab abelian-group-add-ℚ n q + left-mul-rational-nat-ℚ 0 q = left-zero-law-mul-ℚ q + left-mul-rational-nat-ℚ 1 q = left-unit-law-mul-ℚ q + left-mul-rational-nat-ℚ (succ-ℕ n@(succ-ℕ _)) q = + equational-reasoning + rational-ℕ (succ-ℕ n) *ℚ q + ＝ succ-ℚ (rational-ℕ n) *ℚ q + by ap-mul-ℚ (inv (succ-rational-ℕ n)) refl + ＝ q +ℚ rational-ℕ n *ℚ q by + mul-left-succ-ℚ _ _ + ＝ q +ℚ multiple-Ab abelian-group-add-ℚ n q + by ap-add-ℚ refl (left-mul-rational-nat-ℚ n q) + ＝ multiple-Ab abelian-group-add-ℚ (succ-ℕ n) q + by inv (multiple-succ-Ab' abelian-group-add-ℚ n q) +``` + ### `2q = q + q` ```agda abstract mul-two-ℚ : (q : ℚ) → rational-ℕ 2 *ℚ q ＝ q +ℚ q - mul-two-ℚ q = - equational-reasoning - rational-ℤ (one-ℤ +ℤ one-ℤ) *ℚ q - ＝ (one-ℚ +ℚ one-ℚ) *ℚ q by ap (_*ℚ q) (inv (add-rational-ℤ one-ℤ one-ℤ)) - ＝ (one-ℚ *ℚ q) +ℚ (one-ℚ *ℚ q) by right-distributive-mul-add-ℚ _ _ _ - ＝ q +ℚ q by ap-add-ℚ (left-unit-law-mul-ℚ q) (left-unit-law-mul-ℚ q) + mul-two-ℚ = left-mul-rational-nat-ℚ 2 ``` ### The product of a rational number and its denominator is its numerator diff --git a/src/elementary-number-theory/nonzero-natural-numbers.lagda.md b/src/elementary-number-theory/nonzero-natural-numbers.lagda.md index 18887cf415..ec1ccb6309 100644 --- a/src/elementary-number-theory/nonzero-natural-numbers.lagda.md +++ b/src/elementary-number-theory/nonzero-natural-numbers.lagda.md @@ -77,6 +77,14 @@ one-ℕ⁺ : ℕ⁺ one-ℕ⁺ = one-nonzero-ℕ ``` +### The nonzero natural number `2` + +```agda +two-ℕ⁺ : ℕ⁺ +pr1 two-ℕ⁺ = 2 +pr2 two-ℕ⁺ () +``` + ### The successor function on the nonzero natural numbers ```agda diff --git a/src/elementary-number-theory/series-rational-numbers.lagda.md b/src/elementary-number-theory/series-rational-numbers.lagda.md new file mode 100644 index 0000000000..c1f6e8809c --- /dev/null +++ b/src/elementary-number-theory/series-rational-numbers.lagda.md @@ -0,0 +1,102 @@ +# Series of rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.series-rational-numbers where +``` + +
Imports + +```agda +open import analysis.convergent-series-metric-abelian-groups +open import analysis.series-metric-abelian-groups + +open import elementary-number-theory.addition-nonnegative-rational-numbers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.metric-additive-group-of-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.rational-numbers + +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.propositions +open import foundation.universe-levels + +open import lists.sequences + +open import order-theory.increasing-sequences-posets +open import order-theory.order-preserving-maps-posets +``` + +
+ +## Idea + +A {{#concept "series" Disambiguation="in ℚ" Agda=series-ℚ}} of +[rational numbers](elementary-number-theory.rational-numbers.md) is a +[series](analysis.series-metric-abelian-groups.md) in the +[metric additive group of rational numbers](elementary-number-theory.metric-additive-group-of-rational-numbers.md) + +## Definition + +```agda +series-ℚ : UU lzero +series-ℚ = series-Metric-Ab metric-ab-add-ℚ + +series-terms-ℚ : sequence ℚ → series-ℚ +series-terms-ℚ = series-terms-Metric-Ab + +partial-sum-series-ℚ : series-ℚ → ℕ → ℚ +partial-sum-series-ℚ = partial-sum-series-Metric-Ab + +term-series-ℚ : series-ℚ → ℕ → ℚ +term-series-ℚ = term-series-Metric-Ab +``` + +## Properties + +### The proposition that a series converges to a sum + +```agda +is-sum-prop-series-ℚ : series-ℚ → ℚ → Prop lzero +is-sum-prop-series-ℚ = is-sum-prop-series-Metric-Ab + +is-sum-series-ℚ : series-ℚ → ℚ → UU lzero +is-sum-series-ℚ = is-sum-series-Metric-Ab +``` + +### The proposition that a series grows without bound + +```agda +partial-sum-stays-above-prop-series-ℚ : series-ℚ → ℚ → ℕ → Prop lzero +partial-sum-stays-above-prop-series-ℚ σ q n = + Π-Prop ℕ (λ k → leq-ℕ-Prop n k ⇒ leq-ℚ-Prop q (partial-sum-series-ℚ σ k)) + +grows-without-bound-prop-series-ℚ : series-ℚ → Prop lzero +grows-without-bound-prop-series-ℚ σ = + Π-Prop ℚ (λ q → ∃ ℕ (partial-sum-stays-above-prop-series-ℚ σ q)) + +grows-without-bound-series-ℚ : series-ℚ → UU lzero +grows-without-bound-series-ℚ σ = + type-Prop (grows-without-bound-prop-series-ℚ σ) +``` + +### If all elements of a series are nonnegative, its partial sums are increasing + +```agda +abstract + is-increasing-partial-sum-is-nonnegative-term-series-ℚ : + (σ : series-ℚ) → ((n : ℕ) → is-nonnegative-ℚ (term-series-ℚ σ n)) → + is-increasing-sequence-Poset ℚ-Poset (partial-sum-series-ℚ σ) + is-increasing-partial-sum-is-nonnegative-term-series-ℚ σ H = + is-increasing-leq-succ-sequence-Poset + ( ℚ-Poset) + ( partial-sum-series-ℚ σ) + ( λ n → + is-inflationary-map-right-add-rational-ℚ⁰⁺ + ( term-series-ℚ σ n , H n) + ( partial-sum-series-ℚ σ n)) +``` diff --git a/src/elementary-number-theory/sums-of-finite-sequences-of-rational-numbers.lagda.md b/src/elementary-number-theory/sums-of-finite-sequences-of-rational-numbers.lagda.md new file mode 100644 index 0000000000..374a1d8051 --- /dev/null +++ b/src/elementary-number-theory/sums-of-finite-sequences-of-rational-numbers.lagda.md @@ -0,0 +1,109 @@ +# Sums of finite sequences of rational numbers + +```agda +module elementary-number-theory.sums-of-finite-sequences-of-rational-numbers where +``` + +
Imports + +```agda +open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings + +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.ring-of-rational-numbers + +open import foundation.function-types +open import foundation.identity-types + +open import lists.finite-sequences + +open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +The +{{#concept "sum operation" Disambiguation="of a finite sequence of rational numbers" Agda=sum-fin-sequence-ℚ}} +extends [addition](elementary-number-theory.addition-rational-numbers.md) on the +[rational numbers](elementary-number-theory.rational-numbers.md) to any +[finite sequence](lists.finite-sequences.md) of rational numbers. + +## Definition + +```agda +sum-fin-sequence-ℚ : (n : ℕ) → fin-sequence ℚ n → ℚ +sum-fin-sequence-ℚ = sum-fin-sequence-type-Commutative-Ring commutative-ring-ℚ +``` + +## Properties + +### The sum of a constant sequence is multiplication by a natural number + +```agda +abstract + sum-constant-fin-sequence-ℚ : + (n : ℕ) (q : ℚ) → + sum-fin-sequence-ℚ n (λ _ → q) ＝ rational-ℕ n *ℚ q + sum-constant-fin-sequence-ℚ n q = + sum-constant-fin-sequence-type-Commutative-Ring commutative-ring-ℚ n q ∙ + inv (left-mul-rational-nat-ℚ n q) +``` + +### If `aₙ ≤ bₙ` for each `n`, then `Σ aₙ ≤ Σ bₙ` + +```agda +abstract + preserves-leq-sum-fin-sequence-ℚ : + (n : ℕ) (a b : fin-sequence ℚ n) → ((k : Fin n) → leq-ℚ (a k) (b k)) → + leq-ℚ (sum-fin-sequence-ℚ n a) (sum-fin-sequence-ℚ n b) + preserves-leq-sum-fin-sequence-ℚ 0 _ _ _ = refl-leq-ℚ zero-ℚ + preserves-leq-sum-fin-sequence-ℚ (succ-ℕ n) a b H = + preserves-leq-add-ℚ + ( preserves-leq-sum-fin-sequence-ℚ + ( n) + ( a ∘ inl-Fin n) + ( b ∘ inl-Fin n) + ( H ∘ inl-Fin n)) + ( H (neg-one-Fin n)) +``` + +### Multiplication is distributive over sums on finite sequences + +```agda +abstract + left-distributive-mul-sum-fin-sequence-ℚ : + (n : ℕ) (q : ℚ) (a : fin-sequence ℚ n) → + q *ℚ sum-fin-sequence-ℚ n a ＝ sum-fin-sequence-ℚ n (mul-ℚ q ∘ a) + left-distributive-mul-sum-fin-sequence-ℚ = + left-distributive-mul-sum-fin-sequence-type-Commutative-Ring + ( commutative-ring-ℚ) +``` + +### Splitting sums of `n + m` elements into a sum of `n` elements and a sum of `m` elements + +```agda +split-sum-fin-sequence-ℚ : + (n m : ℕ) (f : fin-sequence ℚ (n +ℕ m)) → + sum-fin-sequence-ℚ (n +ℕ m) f ＝ + sum-fin-sequence-ℚ n (f ∘ inl-coproduct-Fin n m) +ℚ + sum-fin-sequence-ℚ m (f ∘ inr-coproduct-Fin n m) +split-sum-fin-sequence-ℚ = + split-sum-fin-sequence-type-Commutative-Ring commutative-ring-ℚ +``` + +### The sum of a single element is the single element + +```agda +compute-sum-one-element-ℚ : + (a : fin-sequence ℚ 1) → sum-fin-sequence-ℚ 1 a ＝ a (zero-Fin 0) +compute-sum-one-element-ℚ = + compute-sum-one-element-Commutative-Ring commutative-ring-ℚ +``` diff --git a/src/elementary-number-theory/triangular-numbers.lagda.md b/src/elementary-number-theory/triangular-numbers.lagda.md index 0a3f74aae1..d7c5a79cef 100644 --- a/src/elementary-number-theory/triangular-numbers.lagda.md +++ b/src/elementary-number-theory/triangular-numbers.lagda.md @@ -9,15 +9,11 @@ module elementary-number-theory.triangular-numbers where
Imports ```agda -open import analysis.convergent-series-metric-abelian-groups -open import analysis.series-metric-abelian-groups - open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.divisibility-natural-numbers -open import elementary-number-theory.metric-additive-group-of-rational-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers @@ -27,6 +23,7 @@ open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.semiring-of-natural-numbers +open import elementary-number-theory.series-rational-numbers open import elementary-number-theory.unit-fractions-rational-numbers open import foundation.action-on-identifications-functions @@ -203,15 +200,14 @@ abstract ( eq-nonzero-ℕ ( compute-double-triangular-number-ℕ (succ-ℕ n))))) -series-reciprocal-triangular-number-ℕ : series-Metric-Ab metric-ab-add-ℚ +series-reciprocal-triangular-number-ℕ : series-ℚ series-reciprocal-triangular-number-ℕ = - series-terms-Metric-Ab reciprocal-triangular-number-succ-ℕ + series-terms-ℚ reciprocal-triangular-number-succ-ℕ abstract compute-partial-sum-series-reciprocal-triangular-number-ℕ : (n : ℕ) → - partial-sum-series-Metric-Ab - ( metric-ab-add-ℚ) + partial-sum-series-ℚ ( series-reciprocal-triangular-number-ℕ) ( n) ＝ rational-ℕ 2 *ℚ (one-ℚ -ℚ reciprocal-rational-succ-ℕ n) @@ -227,8 +223,7 @@ abstract by right-zero-law-mul-ℚ _) compute-partial-sum-series-reciprocal-triangular-number-ℕ (succ-ℕ n) = equational-reasoning - partial-sum-series-Metric-Ab - ( metric-ab-add-ℚ) + partial-sum-series-ℚ ( series-reciprocal-triangular-number-ℕ) ( n) +ℚ reciprocal-triangular-number-succ-ℕ n @@ -271,7 +266,7 @@ This theorem is the [42nd](literature.100-theorems.md#42) theorem on ```agda abstract sum-reciprocal-triangular-number-ℕ : - is-sum-series-Metric-Ab + is-sum-series-ℚ ( series-reciprocal-triangular-number-ℕ) ( rational-ℕ 2) sum-reciprocal-triangular-number-ℕ = diff --git a/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md b/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md index 035a9a963f..8d26e1dcbc 100644 --- a/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md +++ b/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md @@ -119,6 +119,19 @@ module _ ( eq-denominator-reciprocal-rational-ℤ⁺) ``` +### Taking the reciprocal of a nonzero natural number distributes over multiplication + +```agda +abstract + distributive-reciprocal-mul-ℕ⁺ : + (m n : ℕ⁺) → + reciprocal-rational-ℕ⁺ (m *ℕ⁺ n) ＝ + reciprocal-rational-ℕ⁺ m *ℚ reciprocal-rational-ℕ⁺ n + distributive-reciprocal-mul-ℕ⁺ m⁺@(m , _) n⁺@(n , _) = + ap rational-inv-ℚ⁺ (eq-ℚ⁺ (inv (mul-rational-ℕ m n))) ∙ + ap rational-ℚ⁺ (distributive-inv-mul-ℚ⁺ _ _) +``` + ### If `m ≤ n`, the reciprocal of `n` is less than or equal to the reciprocal of `n` ```agda diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md index 266b0d6d45..6eb7fb632f 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md @@ -218,11 +218,11 @@ module _ ```agda abstract - constant-sum-fin-sequence-type-Ab : + sum-constant-fin-sequence-type-Ab : {l : Level} (G : Ab l) (n : ℕ) (x : type-Ab G) → sum-fin-sequence-type-Ab G n (λ _ → x) ＝ multiple-Ab G n x - constant-sum-fin-sequence-type-Ab G = - constant-sum-fin-sequence-type-Group (group-Ab G) + sum-constant-fin-sequence-type-Ab G = + sum-constant-fin-sequence-type-Group (group-Ab G) ``` ## See also diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md index 374bcb0542..2386f64fef 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md @@ -260,13 +260,13 @@ module _ ```agda abstract - constant-sum-fin-sequence-type-Commutative-Monoid : + sum-constant-fin-sequence-type-Commutative-Monoid : {l : Level} (M : Commutative-Monoid l) (n : ℕ) → (x : type-Commutative-Monoid M) → sum-fin-sequence-type-Commutative-Monoid M n (λ _ → x) ＝ power-Commutative-Monoid M n x - constant-sum-fin-sequence-type-Commutative-Monoid M = - constant-sum-fin-sequence-type-Monoid (monoid-Commutative-Monoid M) + sum-constant-fin-sequence-type-Commutative-Monoid M = + sum-constant-fin-sequence-type-Monoid (monoid-Commutative-Monoid M) ``` ## See also diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-groups.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-groups.lagda.md index 33badd9fbc..27101833bb 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-groups.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-groups.lagda.md @@ -184,9 +184,9 @@ split-sum-fin-sequence-type-Group G = ```agda abstract - constant-sum-fin-sequence-type-Group : + sum-constant-fin-sequence-type-Group : {l : Level} (G : Group l) (n : ℕ) (x : type-Group G) → sum-fin-sequence-type-Group G n (λ _ → x) ＝ power-Group G n x - constant-sum-fin-sequence-type-Group G = - constant-sum-fin-sequence-type-Monoid (monoid-Group G) + sum-constant-fin-sequence-type-Group G = + sum-constant-fin-sequence-type-Monoid (monoid-Group G) ``` diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-monoids.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-monoids.lagda.md index 4b58cd16e5..dcf4a4ff64 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-monoids.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-monoids.lagda.md @@ -213,14 +213,14 @@ split-sum-fin-sequence-type-Monoid M n (succ-ℕ m) f = ```agda abstract - constant-sum-fin-sequence-type-Monoid : + sum-constant-fin-sequence-type-Monoid : {l : Level} (M : Monoid l) (n : ℕ) (x : type-Monoid M) → sum-fin-sequence-type-Monoid M n (λ _ → x) ＝ power-Monoid M n x - constant-sum-fin-sequence-type-Monoid M 0 x = refl - constant-sum-fin-sequence-type-Monoid M 1 x = + sum-constant-fin-sequence-type-Monoid M 0 x = refl + sum-constant-fin-sequence-type-Monoid M 1 x = compute-sum-one-element-Monoid M (λ _ → x) - constant-sum-fin-sequence-type-Monoid M (succ-ℕ n@(succ-ℕ _)) x = + sum-constant-fin-sequence-type-Monoid M (succ-ℕ n@(succ-ℕ _)) x = ap-mul-Monoid M - ( constant-sum-fin-sequence-type-Monoid M n x) + ( sum-constant-fin-sequence-type-Monoid M n x) ( refl) ``` diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md index 862d0a1cea..81353f5e14 100644 --- a/src/literature/100-theorems.lagda.md +++ b/src/literature/100-theorems.lagda.md @@ -46,6 +46,15 @@ open import foundation.cantor-schroder-bernstein-decidable-embeddings using ( Cantor-Schröder-Bernstein-WLPO) ``` +### 34. Divergence of the Harmonic Series {#34} + +**Author:** [Louis Wasserman](https://github.com/lowasser) + +```agda +open import elementary-number-theory.harmonic-series-rational-numbers using + ( grows-without-bound-harmonic-series-ℚ) +``` + ### 42. Sum of the Reciprocals of the Triangular Numbers {#42} **Author:** [Louis Wasserman](https://github.com/lowasser) diff --git a/src/order-theory/increasing-sequences-posets.lagda.md b/src/order-theory/increasing-sequences-posets.lagda.md index f822eec21b..da910eecb4 100644 --- a/src/order-theory/increasing-sequences-posets.lagda.md +++ b/src/order-theory/increasing-sequences-posets.lagda.md @@ -15,12 +15,15 @@ open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types open import foundation.propositions +open import foundation.unit-type open import foundation.universe-levels open import lists.sequences open import order-theory.order-preserving-maps-posets +open import order-theory.order-preserving-maps-preorders open import order-theory.posets +open import order-theory.preorders open import order-theory.sequences-posets open import order-theory.subposets ``` @@ -85,6 +88,51 @@ module _ ## Properties +### Sequences that are increasing by induction + +```agda +module _ + {l1 l2 : Level} (P : Preorder l1 l2) + where + + preserves-order-ind-ℕ-Preorder : + (f : ℕ → type-Preorder P) → + ((n : ℕ) → leq-Preorder P (f n) (f (succ-ℕ n))) → + preserves-order-Preorder ℕ-Preorder P f + preserves-order-ind-ℕ-Preorder f H zero-ℕ zero-ℕ p = + refl-leq-Preorder P (f zero-ℕ) + preserves-order-ind-ℕ-Preorder f H zero-ℕ (succ-ℕ m) p = + transitive-leq-Preorder P (f 0) (f m) (f (succ-ℕ m)) + ( H m) + ( preserves-order-ind-ℕ-Preorder f H zero-ℕ m star) + preserves-order-ind-ℕ-Preorder f H (succ-ℕ n) zero-ℕ () + preserves-order-ind-ℕ-Preorder f H (succ-ℕ n) (succ-ℕ m) = + preserves-order-ind-ℕ-Preorder (f ∘ succ-ℕ) (H ∘ succ-ℕ) n m + + hom-ind-ℕ-Preorder : + (f : ℕ → type-Preorder P) → + ((n : ℕ) → leq-Preorder P (f n) (f (succ-ℕ n))) → + hom-Preorder (ℕ-Preorder) P + hom-ind-ℕ-Preorder f H = f , preserves-order-ind-ℕ-Preorder f H + +module _ + {l1 l2 : Level} (P : Poset l1 l2) + where + + preserves-order-ind-ℕ-Poset : + (f : ℕ → type-Poset P) → + ((n : ℕ) → leq-Poset P (f n) (f (succ-ℕ n))) → + preserves-order-Poset ℕ-Poset P f + preserves-order-ind-ℕ-Poset = + preserves-order-ind-ℕ-Preorder (preorder-Poset P) + + hom-ind-ℕ-Poset : + (f : ℕ → type-Poset P) → + ((n : ℕ) → leq-Poset P (f n) (f (succ-ℕ n))) → + hom-Poset (ℕ-Poset) P + hom-ind-ℕ-Poset = hom-ind-ℕ-Preorder (preorder-Poset P) +``` + ### A sequence `u` in a poset is increasing if and only if `uₙ ≤ uₙ₊₁` for all `n : ℕ` ```agda diff --git a/src/ring-theory/arithmetic-series-semirings.lagda.md b/src/ring-theory/arithmetic-series-semirings.lagda.md index af626c0a4d..653e708c38 100644 --- a/src/ring-theory/arithmetic-series-semirings.lagda.md +++ b/src/ring-theory/arithmetic-series-semirings.lagda.md @@ -180,7 +180,7 @@ module _ compute-sum-add-mul-nat-Semiring n = ap-binary ( add-Semiring R) - ( inv (constant-sum-fin-sequence-type-Semiring R (succ-ℕ n) a)) + ( inv (sum-constant-fin-sequence-type-Semiring R (succ-ℕ n) a)) ( ( ap ( λ i → multiple-Semiring R i d) ( htpy-sum-leq-triangular-ℕ n)) ∙ diff --git a/src/ring-theory/sums-of-finite-sequences-of-elements-rings.lagda.md b/src/ring-theory/sums-of-finite-sequences-of-elements-rings.lagda.md index c65dd2c1a7..17eec95acf 100644 --- a/src/ring-theory/sums-of-finite-sequences-of-elements-rings.lagda.md +++ b/src/ring-theory/sums-of-finite-sequences-of-elements-rings.lagda.md @@ -26,6 +26,7 @@ open import linear-algebra.linear-maps-left-modules-rings open import lists.finite-sequences +open import ring-theory.multiples-of-elements-rings open import ring-theory.rings open import ring-theory.sums-of-finite-sequences-of-elements-semirings @@ -254,6 +255,18 @@ module _ ( λ c x → inv (left-distributive-mul-sum-fin-sequence-type-Ring R n c x)) ``` +### The sum of a constant finite sequence in a ring is scalar multiplication by the length of the sequence + +```agda +abstract + sum-constant-fin-sequence-type-Ring : + {l : Level} (R : Ring l) (n : ℕ) (x : type-Ring R) → + sum-fin-sequence-type-Ring R n (λ _ → x) ＝ + multiple-Ring R n x + sum-constant-fin-sequence-type-Ring R = + sum-constant-fin-sequence-type-Semiring ( semiring-Ring R) +``` + ## See also - [Sums of finite families of elements in rings](ring-theory.sums-of-finite-families-of-elements-rings.md) diff --git a/src/ring-theory/sums-of-finite-sequences-of-elements-semirings.lagda.md b/src/ring-theory/sums-of-finite-sequences-of-elements-semirings.lagda.md index fc420c7089..be44be3ed9 100644 --- a/src/ring-theory/sums-of-finite-sequences-of-elements-semirings.lagda.md +++ b/src/ring-theory/sums-of-finite-sequences-of-elements-semirings.lagda.md @@ -286,12 +286,12 @@ module _ ```agda abstract - constant-sum-fin-sequence-type-Semiring : + sum-constant-fin-sequence-type-Semiring : {l : Level} (R : Semiring l) (n : ℕ) (x : type-Semiring R) → sum-fin-sequence-type-Semiring R n (λ _ → x) ＝ multiple-Semiring R n x - constant-sum-fin-sequence-type-Semiring R = - constant-sum-fin-sequence-type-Commutative-Monoid + sum-constant-fin-sequence-type-Semiring R = + sum-constant-fin-sequence-type-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ``` diff --git a/src/set-theory/increasing-binary-sequences.lagda.md b/src/set-theory/increasing-binary-sequences.lagda.md index f82b214c0a..76aadf1404 100644 --- a/src/set-theory/increasing-binary-sequences.lagda.md +++ b/src/set-theory/increasing-binary-sequences.lagda.md @@ -39,6 +39,7 @@ open import foundation.universe-levels open import foundation-core.identity-types +open import order-theory.increasing-sequences-posets open import order-theory.order-preserving-maps-posets open import set-theory.cantor-space