def recursiveSeq (f : ℕ → ℝ) (c : ℝ) : Prop

Equations

• recursiveSeq f c = ((0 ≤ c ∧ c < 1) ∧ ∀ (n : ℕ), 0 ≤ f n ∧ f (n + 1) ≤ c * f n)

theorem cToZero (c : ℝ) : 0 ≤ c ∧ c < 1 → ∀ ε > 0, ∃ (N : ℕ), ∀ k ≥ N, c ^ k < ε

A computational study of a class of recursive inequalities

MORENIKEJI NERI and THOMAS POWELL

Kjos-Hanssen's part. 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: