A computational study of a class of recursive inequalities #

We formalize the first example from the paper.

theorem firstExampleNeri (μ : ℕ → NNReal) (c : ↑(Set.Ico 0 1)) (h : ∀ (n : ℕ), ↑(μ (n + 1)) ≤ ↑c * ↑(μ n)) (n : ℕ) :

↑(μ n) ≤ ↑c ^ n * ↑(μ 0)

theorem firstExampleNeri_general (μ : ℕ → ℝ) (c : NNReal) (h : ∀ (n : ℕ), μ (n + 1) ≤ ↑c * μ n) (n : ℕ) :

μ n ≤ ↑c ^ n * μ 0

For the inequality to hold we do not need to use the type NNReal but can also use Real; and we can generalize c as well:

Documentation