A recursion that forces a sequence to zero

If u (n+1) ≤ (1 - a (n+1)) * u n + e (n+1) with 0 ≤ a n ≤ 1, the partial sums of a unbounded and e summable, then u n → 0. This drives the hole argument: the measure of what survives the level-n holes contracts by a factor 1 - c/n at each level, up to a summable error, and ∑ 1/n = ∞.

theorem LeanPool.Besicovitch.Example.le_prod_mul_add_sum_of_recursive {u a e : ℕ → ℝ} (ha : ∀ (n : ℕ), 0 ≤ a n) (ha1 : ∀ (n : ℕ), a n ≤ 1) (he : ∀ (n : ℕ), 0 ≤ e n) (h : ∀ (n : ℕ), u (n + 1) ≤ (1 - a (n + 1)) * u n + e (n + 1)) (N n : ℕ) : N ≤ n → u n ≤ (∏ k ∈ Finset.Ioc N n, (1 - a k)) * u N + ∑ k ∈ Finset.Ioc N n, e k

Unrolling the recursion from level N to level n.

theorem LeanPool.Besicovitch.Example.prod_one_sub_le_exp_neg_sum {a : ℕ → ℝ} (ha1 : ∀ (n : ℕ), a n ≤ 1) (s : Finset ℕ) : ∏ k ∈ s, (1 - a k) ≤ Real.exp (-∑ k ∈ s, a k)

A product of 1 - a k is at most exp (-∑ a k).

theorem LeanPool.Besicovitch.Example.tendsto_sum_Ioc_atTop {a : ℕ → ℝ} (hasum : Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, a k) Filter.atTop Filter.atTop) (N : ℕ) : Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.Ioc N n, a k) Filter.atTop Filter.atTop

The sums ∑_{k ∈ Ioc N n} a k tend to infinity when the partial sums of a do.

theorem LeanPool.Besicovitch.Example.tendsto_zero_of_recursive {u a e : ℕ → ℝ} (hu : ∀ (n : ℕ), 0 ≤ u n) (ha : ∀ (n : ℕ), 0 ≤ a n) (ha1 : ∀ (n : ℕ), a n ≤ 1) (he : ∀ (n : ℕ), 0 ≤ e n) (hasum : Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range n, a k) Filter.atTop Filter.atTop) (hesum : Summable e) (h : ∀ (n : ℕ), u (n + 1) ≤ (1 - a (n + 1)) * u n + e (n + 1)) : Filter.Tendsto u Filter.atTop (nhds 0)

The main recursion lemma.