The challenge and response maps

This file proves the reduction from concrete finite block catalogues to slaloms. The analytic hypotheses are precisely the conclusions of the finite construction; they do not assume an inequality between cardinal characteristics.

structure NonMRR.BlockCatalogue (r : ℕ → ℕ) (b : ℕ → ℝ) : Type

The concrete finite block data needed by the construction, for every g.

• interval : (ℕ → ℕ) → ℕ → Finset ℕ

  The disjoint finite coordinate block at each stage.

• vector : (ℕ → ℕ) → ℕ → ℕ → ℕ → ℝ

  The balanced vectors supported on the stage blocks.

• disjoint (g : ℕ → ℕ) : Pairwise fun (n m : ℕ) => Disjoint (self.interval g n) (self.interval g m)
• support (g : ℕ → ℕ) (n k : ℕ) : k < g n → ∀ i ∉ self.interval g n, self.vector g n k i = 0
• balance (g : ℕ → ℕ) (n k : ℕ) : k < g n → ∑ i ∈ self.interval g n, self.vector g n k i = 0
• mass (g : ℕ → ℕ) (n k : ℕ) : k < g n → 1 ≤ ∑ i ∈ self.interval g n, ‖self.vector g n k i‖
• bad_card (g : ℕ → ℕ) (π : Equiv.Perm ℕ) (n : ℕ) : (badValues (self.vector g) g π b n).card ≤ r n

noncomputable def NonMRR.BlockCatalogue.candidate {r : ℕ → ℕ} {b : ℕ → ℝ} (C : BlockCatalogue r b) (e g : ℕ → ℕ) (i : ℕ) : ℝ

The selected series, before testing its convergence.

Equations

• C.candidate e g i = ∑' (n : ℕ), NonMRR.selectedBlock (C.vector g) e g n i

noncomputable def NonMRR.BlockCatalogue.response {r : ℕ → ℕ} {b : ℕ → ℝ} (C : BlockCatalogue r b) (p : (ℕ → ℕ) × Equiv.Perm ℕ) : Slalom r

The exceptional-value slalom assigned to a growth function and a permutation.

Equations

• C.response p = ⟨NonMRR.badValues (C.vector p.1) p.1 p.2 b, ⋯⟩

def NonMRR.BlockCatalogue.CandidateGood {r : ℕ → ℕ} {b : ℕ → ℝ} (C : BlockCatalogue r b) (e g : ℕ → ℕ) : Prop

A property used to select the genuine challenge or a fixed fallback challenge.

Equations

• C.CandidateGood e g = (Filter.Tendsto (NonMRR.partialSum (C.candidate e g)) Filter.atTop (nhds 0) ∧ ¬Summable fun (i : ℕ) => |C.candidate e g i|)

noncomputable def NonMRR.BlockCatalogue.challengeSeries {r : ℕ → ℕ} {b : ℕ → ℝ} (C : BlockCatalogue r b) (e g : ℕ → ℕ) : ConditionalSeries

The fallback ensures that the challenge map is defined even for bad choices of g.

Equations

• C.challengeSeries e g = if h : C.CandidateGood e g then { term := C.candidate e g, sum := 0, converges := ⋯, not_absolute := ⋯ } else Classical.choice NonMRR.conditionalSeries_nonempty

theorem NonMRR.BlockCatalogue.candidate_good_of_avoids {r : ℕ → ℕ} {b : ℕ → ℝ} (C : BlockCatalogue r b) (hb : Summable b) (hbnonneg : ∀ (n : ℕ), 0 ≤ b n) (e g : ℕ → ℕ) (π : Equiv.Perm ℕ) (hinfinite : FrequentlyLT e g) (havoid : ∀ᶠ (n : ℕ) in Filter.atTop, e n ∉ ↑(C.response (g, π)) n) : C.CandidateGood e g ∧ Filter.Tendsto (partialSum (C.candidate e g ∘ ⇑π)) Filter.atTop (nhds 0)

Eventual avoidance gives the required common zero-sum witness.

theorem NonMRR.BlockCatalogue.catches_of_rearranges {r : ℕ → ℕ} {b : ℕ → ℝ} (C : BlockCatalogue r b) (hb : Summable b) (hbnonneg : ∀ (n : ℕ), 0 ≤ b n) (e g : ℕ → ℕ) (π : Equiv.Perm ℕ) (hinfinite : FrequentlyLT e g) (hπ : Rearranges (C.challengeSeries e g) π) : ∃ᶠ (n : ℕ) in Filter.atTop, e n ∈ ↑(C.response (g, π)) n

The central implication in the morphism: a rearrangement forces infinitely many catches by its exceptional-value slalom.

theorem NonMRR.BlockCatalogue.dominating_response_image {r : ℕ → ℕ} {b : ℕ → ℝ} (C : BlockCatalogue r b) (hr : ∀ (n : ℕ), 0 < r n) (hb : Summable b) (hbnonneg : ∀ (n : ℕ), 0 ≤ b n) {G : Set (ℕ → ℕ)} {P : Set (Equiv.Perm ℕ)} (hG : boundingRelation.Dominating G) (hP : IsRearranging P) : (slalomRelation r hr).Dominating (C.response '' G ×ˢ P)

Images of an unbounded family and a rearranging family dominate the slalom relation.

theorem NonMRR.BlockCatalogue.slalom_norm_le_bounding_mul_cardinal {r : ℕ → ℕ} {b : ℕ → ℝ} (C : BlockCatalogue r b) (hr : ∀ (n : ℕ), 0 < r n) (hb : Summable b) (hbnonneg : ∀ (n : ℕ), 0 ≤ b n) {P : Set (Equiv.Perm ℕ)} (hP : IsRearranging P) : (slalomRelation r hr).norm ≤ boundingNumber * Cardinal.mk ↑P

The cardinal bound before applying the classical inequality b ≤ rr.