Rearranging a conditionally convergent series through Baire category.

theorem NonMRR.summable_abs_of_bounded_finite_sums (a : ℕ → ℝ) (c : ℝ) (h : ∀ (s : Finset ℕ), |∑ i ∈ s, a i| ≤ c) : Summable fun (i : ℕ) => |a i|

A real family with bounded sums on all finite subsets is absolutely summable.

theorem NonMRR.exists_large_finite_sum (a : ℕ → ℝ) (ha : ¬Summable fun (i : ℕ) => |a i|) (c : ℝ) : ∃ (s : Finset ℕ), c < |∑ i ∈ s, a i|

Nonabsolute summability forces arbitrarily large finite sums.

theorem NonMRR.exists_large_finite_sum_disjoint (a : ℕ → ℝ) (ha : ¬Summable fun (i : ℕ) => |a i|) (F : Finset ℕ) (c : ℝ) : ∃ (s : Finset ℕ), Disjoint s F ∧ c < |∑ i ∈ s, a i|

The same unboundedness holds after excluding any prescribed finite set.

theorem NonMRR.exists_perm_large_partialSum (a : ℕ → ℝ) (ha : ¬Summable fun (i : ℕ) => |a i|) (f : ℕ → ℕ) (hf : Function.Injective f) (N : ℕ) (c : ℝ) : ∃ (π : Equiv.Perm ℕ), (∀ i < N, π i = f i) ∧ ∃ (M : ℕ), c < |partialSum (a ∘ ⇑π) M|

Extend any finite initial segment of an injection to a permutation having an arbitrarily large partial sum.

@[reducible, inline]

abbrev NonMRR.InjectionSpace : Type

The space of injective enumerations of natural numbers.

Equations

• NonMRR.InjectionSpace = { f : ℕ → ℕ // Function.Injective f }

theorem NonMRR.isClosed_injections : IsClosed {f : ℕ → ℕ | Function.Injective f}

instance NonMRR.instIsCompletelyMetrizableSpaceInjectionSpace : TopologicalSpace.IsCompletelyMetrizableSpace InjectionSpace

instance NonMRR.instNonemptyInjectionSpace : Nonempty InjectionSpace

theorem NonMRR.dense_injections_of_extension (P : Set InjectionSpace) (h : ∀ (f : InjectionSpace) (N : ℕ), ∃ g ∈ P, ∀ i < N, ↑g i = ↑f i) : Dense P

A useful density criterion for the closed space of injections.