The cardinal conclusion for the concrete slalom relation

This is the analytic/combinatorial reduction of the manuscript, including the classical bounding-number lower bound. The category comparison needed for the topological cardinal nonM is proved in NonMRR.CategoryBound.

noncomputable def NonMRR.blockSlalomNumber : Cardinal.{0}

The norm of the specific bounded-slalom relation used in the construction.

Equations

• NonMRR.blockSlalomNumber = (NonMRR.slalomRelation NonMRR.blockCapacity NonMRR.blockCapacity_pos).norm

theorem NonMRR.blockSlalomNumber_le_cardinal_of_isRearranging {P : Set (Equiv.Perm ℕ)} (hP : IsRearranging P) : blockSlalomNumber ≤ Cardinal.mk ↑P

Every rearranging family has size at least the norm of the block slaloms.

theorem NonMRR.exists_preserved_series_of_cardinal_lt_blockSlalomNumber {P : Set (Equiv.Perm ℕ)} (hP : Cardinal.mk ↑P < blockSlalomNumber) : ∃ (a : ConditionalSeries), ∀ π ∈ P, HasSum (a.term ∘ ⇑π) a.sum (SummationFilter.conditional ℕ)

A family smaller than the block-slalom norm preserves some conditional series.