A rearrangement with unbounded partial sums

The finite extension lemma supplies dense open conditions in the complete space of injections. Simultaneously requiring each integer in the range turns the resulting injection into a permutation.

theorem NonMRR.continuous_partialSum_on_injections (a : ℕ → ℝ) (M : ℕ) : Continuous fun (f : InjectionSpace) => partialSum (a ∘ ↑f) M

theorem NonMRR.exists_perm_unbounded_partialSum (a : ℕ → ℝ) (ha : ¬Summable fun (i : ℕ) => |a i|) : ∃ (π : Equiv.Perm ℕ), ∀ (k : ℕ), ∃ (M : ℕ), ↑k < |partialSum (a ∘ ⇑π) M|

Every real sequence which is not absolutely summable has a permutation with unbounded absolute partial sums.

theorem NonMRR.exists_rearranges (a : ConditionalSeries) : ∃ (π : Equiv.Perm ℕ), Rearranges a π

Every conditionally convergent series is rearranged by some permutation.

theorem NonMRR.forall_exists_rearranges (a : ConditionalSeries) : ∃ (π : Equiv.Perm ℕ), Rearranges a π

theorem NonMRR.isRearranging_univ : IsRearranging Set.univ

All permutations form a rearranging family.

theorem NonMRR.exists_rearranging_family : ∃ (P : Set (Equiv.Perm ℕ)), IsRearranging P