Inserting zero terms along an eventually increasing injection

An arbitrary reordering of finitely many initial terms is harmless. Consequently an injective placement that is increasing beyond a finite index preserves the natural sum of a series, and inserting zeros preserves failure of absolute convergence.

noncomputable def NonMRR.paddingPreimage (t : ℕ → ℕ) (ht : Function.Injective t) (j : ℕ) : Finset ℕ

The finite set of original indices visited before position j.

Equations

• NonMRR.paddingPreimage t ht j = (Finset.range j).preimage t ⋯

@[simp]

theorem NonMRR.mem_paddingPreimage (t : ℕ → ℕ) (ht : Function.Injective t) (j n : ℕ) : n ∈ paddingPreimage t ht j ↔ t n < j

theorem NonMRR.eventually_range_subset_paddingPreimage (t : ℕ → ℕ) (ht : Function.Injective t) (N : ℕ) : ∀ᶠ (j : ℕ) in Filter.atTop, Finset.range N ⊆ paddingPreimage t ht j

theorem NonMRR.tendsto_card_paddingPreimage (t : ℕ → ℕ) (ht : Function.Injective t) : Filter.Tendsto (fun (j : ℕ) => (paddingPreimage t ht j).card) Filter.atTop Filter.atTop

theorem NonMRR.eventually_paddingPreimage_eq_range (t : ℕ → ℕ) (ht : Function.Injective t) (N : ℕ) (hmono : ∀ n ≥ N, ∀ (m : ℕ), n < m → t n < t m) : ∀ᶠ (j : ℕ) in Filter.atTop, paddingPreimage t ht j = Finset.range (paddingPreimage t ht j).card

Beyond the finitely many exceptional positions, the original indices already visited form an initial segment.

theorem NonMRR.partialSum_extend_eq_preimage (b : ℕ → ℝ) (t : ℕ → ℕ) (ht : Function.Injective t) (j : ℕ) : partialSum (Function.extend t b 0) j = ∑ n ∈ paddingPreimage t ht j, b n

theorem NonMRR.tendsto_partialSum_extend (b : ℕ → ℝ) (t : ℕ → ℕ) (ht : Function.Injective t) (N : ℕ) (hmono : ∀ n ≥ N, ∀ (m : ℕ), n < m → t n < t m) (s : ℝ) (hb : Filter.Tendsto (partialSum b) Filter.atTop (nhds s)) : Filter.Tendsto (partialSum (Function.extend t b 0)) Filter.atTop (nhds s)

Inserting zeros along an eventually increasing injection preserves the natural sum.

theorem NonMRR.not_summable_abs_extend (b : ℕ → ℝ) (t : ℕ → ℕ) (ht : Function.Injective t) (hb : ¬Summable fun (n : ℕ) => |b n|) : ¬Summable fun (n : ℕ) => |Function.extend t b 0 n|

Inserting zeros along an injection preserves failure of absolute convergence.