The rearrangement number

Convergence is taken along the natural partial sums. In particular, ordinary Summable a would be the wrong definition of conditional convergence over ℝ. We use mathlib's SummationFilter.conditional ℕ explicitly.

def NonMRR.partialSum (a : ℕ → ℝ) (n : ℕ) : ℝ

The sum of the first n terms.

Equations

• NonMRR.partialSum a n = ∑ i ∈ Finset.range n, a i

theorem NonMRR.hasSum_conditional_iff {a : ℕ → ℝ} {s : ℝ} : HasSum a s (SummationFilter.conditional ℕ) ↔ Filter.Tendsto (partialSum a) Filter.atTop (nhds s)

structure NonMRR.ConditionalSeries : Type

A real series together with its unique natural sum and conditional convergence proofs.

• term : ℕ → ℝ

  The sequence of terms of the series.

• sum : ℝ

  The sum in the natural ordering of the terms.

• converges : HasSum self.term self.sum (SummationFilter.conditional ℕ)
• not_absolute : ¬Summable fun (n : ℕ) => |self.term n|

def NonMRR.Rearranges (a : ConditionalSeries) (π : Equiv.Perm ℕ) : Prop

A permutation rearranges a series when it fails to preserve its natural sum.

Equations

• NonMRR.Rearranges a π = ¬HasSum (a.term ∘ ⇑π) a.sum (SummationFilter.conditional ℕ)

def NonMRR.IsRearranging (s : Set (Equiv.Perm ℕ)) : Prop

A family which rearranges every conditionally convergent real series.

Equations

• NonMRR.IsRearranging s = ∀ (a : NonMRR.ConditionalSeries), ∃ π ∈ s, NonMRR.Rearranges a π

noncomputable def NonMRR.rr : Cardinal.{0}

The rearrangement number, with the cardinal-minimum definition in the manuscript.

Equations

• NonMRR.rr = sInf {κ : Cardinal.{0} | ∃ (s : Set (Equiv.Perm ℕ)), NonMRR.IsRearranging s ∧ Cardinal.mk ↑s = κ}

theorem NonMRR.rr_le_cardinal {s : Set (Equiv.Perm ℕ)} (hs : IsRearranging s) : rr ≤ Cardinal.mk ↑s

theorem NonMRR.not_isRearranging_of_preserves {s : Set (Equiv.Perm ℕ)} (a : ConditionalSeries) (h : ∀ π ∈ s, HasSum (a.term ∘ ⇑π) a.sum (SummationFilter.conditional ℕ)) : ¬IsRearranging s

A common preserved series witnesses that a family is not rearranging.

theorem NonMRR.not_isRearranging_of_zero_witness {s : Set (Equiv.Perm ℕ)} {a : ℕ → ℝ} (ha : Filter.Tendsto (partialSum a) Filter.atTop (nhds 0)) (hab : ¬Summable fun (n : ℕ) => |a n|) (hπ : ∀ π ∈ s, Filter.Tendsto (partialSum (a ∘ ⇑π)) Filter.atTop (nhds 0)) : ¬IsRearranging s

A witness whose natural and rearranged sums are zero has the required semantics.

theorem NonMRR.conditionalSeries_nonempty : Nonempty ConditionalSeries

The alternating harmonic series supplies an actual challenge.