Bernoulli's inequality on the positive rational numbers

[malarbol]

This PR implements some of my suggestions from #1354 (comment)

• group-theory.arithmetic-sequences-semigroups:

  • sequences in a semigroup with a common difference: uₙ₊₁ = uₙ + d;
  • standard arithmetic sequences given by initial value and common difference;
  • homotopy between arithmetic sequences with same initial value and common difference.

• elementary-number-theory.arithmetic-sequences-positive-rational-numbers:

  • arithmetic sequences in the additive semigroup of positive rational numbers;
  • basic properties;
  • computational rule uₙ = u₀ + n d;
  • an arithmetic sequence in ℚ⁺ is strictly increasing.

• elementary-number-theory.geometric-sequences-positive-rational-numbers:

  • arithmetic sequences in the multiplicative semigroup of positive rational numbers;
  • basic properties;
  • computational rule uₙ = u₀ rⁿ ;
  • constant sequences are geometric;
  • geometric sequences with common ratio r > 1 are strictly increasing;
  • multiplication of geometric sequences in ℚ⁺;
  • inversion of geometric sequences in ℚ⁺.

• elementary-number-theory.bernoullis-inequality-positive-rational-numbers:

  • ∀ (h : ℚ⁺) (n : ℕ) → 1 + (n + 1)h ≤ (1 + n h)(1 + h);
  • Bernoulli's inequality in ℚ⁺: ∀ (h : ℚ⁺) (n : ℕ) → 1 + n h ≤ (1 + h)ⁿ.

[malarbol]

Hi @fredrik-bakke! I hope you are doing well.
This is the follow-up of my comment in #1354 (comment) . I finally went through the technical details and wrote a few proof that will probably help us doing real analysis.

The next steps would probably be to work with geometric series, if we prove (1 - r)(1 + r + ... + rⁿ) = 1 - rⁿ⁺¹ we could prove the convergence of positive rational geometric series. We should also build some similar machinery for the positive real numbers but we'll need addition and multiplication. Let's talk about it ;)

PS: I have no idea why the link-check doesn't pass. Do you have any tip? Also, the typechecking seems a bit long; I guess we'll have to abstract a few proofs but I don't really know which one.

[VojtechStep]

I have no idea why the link-check doesn't pass

"Concept definition not found: arithmetic sequence ; expected "arithmetic-sequence-ℚ⁺" to exist in elementary-number-theory.arithmetic-sequences-positive-rational-numbers.md" means that there's an issue with the {{#concept}} tag for that definition. The problem here is that the Agda=xyz part shouldn't have quotes around xyz.

we'll have to abstract a few proofs but I don't really know which one

Unless you really need to calculate with the definition, probably at least proofs of inequalities should be abstract

[malarbol]

The problem here is that the Agda=xyz part shouldn't have quotes around xyz.

oh! I see. sorry, you could have caught that!

Unless you really need to calculate with the definition, probably at least proofs of inequalities should be abstract

ok. I'll do that. thanks a lot!

[fredrik-bakke]

Very nice additions!