Analytic lemmas for the block construction

Convergence of a real series is expressed through its ordered partial sums. In particular, the conclusion below is deliberately a Tendsto statement: Summable for real series would assert unconditional (absolute) convergence.

def NonMRR.rearrangedPartialSum (a : ℕ → ℝ) (π : Equiv.Perm ℕ) (j : ℕ) : ℝ

The partial sum of a series in the order specified by a permutation.

Equations

• NonMRR.rearrangedPartialSum a π j = ∑ i ∈ Finset.range j, a (π i)

theorem NonMRR.summable_blocks_at_coordinate (u : ℕ → ℕ → ℝ) (I : ℕ → Finset ℕ) (hdisjoint : Pairwise fun (n m : ℕ) => Disjoint (I n) (I m)) (hsupport : ∀ (n i : ℕ), i ∉ I n → u n i = 0) (i : ℕ) : Summable fun (n : ℕ) => u n i

A coordinate belongs to at most one member of a disjoint block family.

theorem NonMRR.tsum_blocks_eq_of_mem (u : ℕ → ℕ → ℝ) (I : ℕ → Finset ℕ) (hdisjoint : Pairwise fun (n m : ℕ) => Disjoint (I n) (I m)) (hsupport : ∀ (n i : ℕ), i ∉ I n → u n i = 0) (n i : ℕ) (hi : i ∈ I n) : ∑' (m : ℕ), u m i = u n i

The coordinatewise sum of disjoint blocks equals the unique relevant block.

theorem NonMRR.tendsto_zero_of_dominated_blocks (u : ℕ → ℕ → ℝ) (π : Equiv.Perm ℕ) (hzero : ∀ (n : ℕ), HasSum (u n) 0) (hlocal : ∀ (i : ℕ), Summable fun (n : ℕ) => u n i) (b : ℕ → ℝ) (hb : Summable b) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (j : ℕ), ‖rearrangedPartialSum (u n) π j‖ ≤ b n) : Filter.Tendsto (rearrangedPartialSum (fun (i : ℕ) => ∑' (n : ℕ), u n i) π) Filter.atTop (nhds 0)

Summably dominated blocks with sum zero have total ordered sum zero.

The domination may fail at finitely many block indices. The local summability hypothesis is automatic for pairwise disjoint finite supports.

theorem NonMRR.not_summable_norm_of_disjoint_blocks (a : ℕ → ℝ) (I : ℕ → Finset ℕ) (A : Set ℕ) (hA : A.Infinite) (hdisjoint : A.PairwiseDisjoint I) (hmass : ∀ n ∈ A, 1 ≤ ∑ i ∈ I n, ‖a i‖) : ¬Summable fun (i : ℕ) => ‖a i‖

Infinitely many disjoint blocks of absolute mass at least one prevent absolute convergence. The blocks need not be intervals.

theorem NonMRR.conditional_series_of_disjoint_balanced_blocks (u : ℕ → ℕ → ℝ) (I : ℕ → Finset ℕ) (A : Set ℕ) (π : Equiv.Perm ℕ) (hdisjoint : Pairwise fun (n m : ℕ) => Disjoint (I n) (I m)) (hsupport : ∀ (n i : ℕ), i ∉ I n → u n i = 0) (hbalance : ∀ (n : ℕ), ∑ i ∈ I n, u n i = 0) (hA : A.Infinite) (hmass : ∀ n ∈ A, 1 ≤ ∑ i ∈ I n, ‖u n i‖) (b : ℕ → ℝ) (hb : Summable b) (hid : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (j : ℕ), ‖rearrangedPartialSum (u n) (Equiv.refl ℕ) j‖ ≤ b n) (hπ : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (j : ℕ), ‖rearrangedPartialSum (u n) π j‖ ≤ b n) : have a := fun (i : ℕ) => ∑' (n : ℕ), u 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‖

The analytic conclusion used in the slalom construction: disjoint balanced finite blocks, uniformly small outside finitely many indices in both relevant orders, give a conditionally convergent series whose sum the permutation preserves.