The morphism into the slaloms

This is the explicit Galois–Tukey morphism of Lemma 4.1 in the manuscript. Its challenge map sends e to e together with the conditional series selected from each catalogue indexed by g. Its response map records the exceptional blocks of a growth function and a permutation.

def NonMRR.rearrangementRelation : Relation

The rearrangement relation on conditionally convergent real series. The rearrangement theorem supplies a response to every challenge.

Equations

• NonMRR.rearrangementRelation = { Challenge := NonMRR.ConditionalSeries, Response := Equiv.Perm ℕ, relates := NonMRR.Rearranges, total := NonMRR.exists_rearranges }

theorem NonMRR.rearrangementRelation_norm_eq_rr : rearrangementRelation.norm = rr

The relation norm agrees with the cardinal-minimum definition of rr.

noncomputable def NonMRR.blockMorphism : (boundingRelation.sequential rearrangementRelation).Morphism (slalomRelation blockCapacity blockCapacity_pos)

The explicit morphism from the sequential bounding/rearrangement relation to slaloms of width 8 * (2^(n+1))^4.

Equations

• One or more equations did not get rendered due to their size.

theorem NonMRR.blockCapacity_tendsto_atTop : Filter.Tendsto blockCapacity Filter.atTop Filter.atTop

The concrete width bound of the block construction tends to infinity.

theorem NonMRR.exists_divergent_slalom_morphism : ∃ (r : ℕ → ℕ) (hr : ∀ (n : ℕ), 0 < r n), Filter.Tendsto r Filter.atTop Filter.atTop ∧ Nonempty ((boundingRelation.sequential rearrangementRelation).Morphism (slalomRelation r hr))

Lemma 4.1: a positive width tending to infinity admits a morphism from the sequential bounding/rearrangement relation into its slalom relation.