Selecting the good blocks

This file formalizes the implication from eventual avoidance of the bad-value slalom to a common zero-sum witness. All hypotheses describe the concrete finite blocks and the chosen functions; no cardinal-invariant inequality is assumed.

def NonMRR.selectedBlock (u : ℕ → ℕ → ℕ → ℝ) (e g : ℕ → ℕ) (n i : ℕ) : ℝ

Choose block e n if it is available, and use the zero block otherwise.

Equations

• NonMRR.selectedBlock u e g n i = if e n < g n then u n (e n) i else 0

noncomputable def NonMRR.badValues (u : ℕ → ℕ → ℕ → ℝ) (g : ℕ → ℕ) (π : Equiv.Perm ℕ) (b : ℕ → ℝ) (n : ℕ) : Finset ℕ

Values with a large prefix in the natural or the permuted order.

Equations

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

theorem NonMRR.prefix_bounds_of_not_mem_badValues (u : ℕ → ℕ → ℕ → ℝ) (g : ℕ → ℕ) (π : Equiv.Perm ℕ) (b : ℕ → ℝ) (n k : ℕ) (hk : k < g n) (hgood : k ∉ badValues u g π b n) : (∀ (j : ℕ), ‖rearrangedPartialSum (u n k) (Equiv.refl ℕ) j‖ ≤ b n) ∧ ∀ (j : ℕ), ‖rearrangedPartialSum (u n k) π j‖ ≤ b n

Avoiding a bad value bounds every prefix in both orders.

theorem NonMRR.selected_blocks_give_zero_witness (u : ℕ → ℕ → ℕ → ℝ) (I : ℕ → Finset ℕ) (e g : ℕ → ℕ) (π : Equiv.Perm ℕ) (hdisjoint : Pairwise fun (n m : ℕ) => Disjoint (I n) (I m)) (hsupport : ∀ (n k : ℕ), k < g n → ∀ i ∉ I n, u n k i = 0) (hbalance : ∀ (n k : ℕ), k < g n → ∑ i ∈ I n, u n k i = 0) (hmass : ∀ (n k : ℕ), k < g n → 1 ≤ ∑ i ∈ I n, ‖u n k i‖) (b : ℕ → ℝ) (hb : Summable b) (hbnonneg : ∀ (n : ℕ), 0 ≤ b n) (hinfinite : ∃ᶠ (n : ℕ) in Filter.atTop, e n < g n) (havoid : ∀ᶠ (n : ℕ) in Filter.atTop, e n ∉ badValues u g π b n) : have a := fun (i : ℕ) => ∑' (n : ℕ), selectedBlock u e g n i; Filter.Tendsto (rearrangedPartialSum a (Equiv.refl ℕ)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (rearrangedPartialSum a π) Filter.atTop (nhds 0) ∧ ¬Summable fun (i : ℕ) => ‖a i‖

Infinitely many selected blocks and eventual avoidance of the bad-value slalom produce a conditionally convergent series with natural and permuted sum zero.