Block-density filters for the Wallace construction

This file packages the density-one filter used in the paper. The formulation is deliberately abstract in the finite blocks: the later scheduling module only has to provide nonempty blocks which eventually avoid every finite set and a deletion bound whose relative size tends to zero.

structure Wallace.BlockSystem : Type

Finite blocks which move to infinity.

• block : ℕ → Finset ℕ

  The finite block carrying a given natural-number label.

• block_nonempty (l : ℕ) : (self.block l).Nonempty
• eventually_disjoint_finite (K : Finset ℕ) : {l : ℕ | Disjoint (self.block l) K} ∈ Filter.atTop

def Wallace.BlockSystem.ofBlockPositions (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) : BlockSystem

The concrete block system supplied by the triangular preprocessing enumeration. Its blocks have the prescribed cardinalities and partition ℕ; in particular, every finite set of positions meets only finitely many block labels.

Equations

• Wallace.BlockSystem.ofBlockPositions N hN = { block := Wallace.TriangularPreprocess.blockPositions N hN, block_nonempty := ⋯, eventually_disjoint_finite := ⋯ }

@[simp]

theorem Wallace.BlockSystem.ofBlockPositions_block (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (l : ℕ) : (ofBlockPositions N hN).block l = TriangularPreprocess.blockPositions N hN l

theorem Wallace.BlockSystem.ofBlockPositions_card (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (l : ℕ) : ((ofBlockPositions N hN).block l).card = N l

noncomputable def Wallace.BlockSystem.missingRatio (B : BlockSystem) (A : Set ℕ) (l : ℕ) : ℝ

Proportion of a block missing from a set.

Equations

• B.missingRatio A l = ↑{n ∈ B.block l | n ∉ A}.card / ↑(B.block l).card

theorem Wallace.BlockSystem.missingRatio_nonneg (B : BlockSystem) (A : Set ℕ) (l : ℕ) : 0 ≤ B.missingRatio A l

@[simp]

theorem Wallace.BlockSystem.missingRatio_univ (B : BlockSystem) (l : ℕ) : B.missingRatio Set.univ l = 0

@[simp]

theorem Wallace.BlockSystem.missingRatio_empty (B : BlockSystem) (l : ℕ) : B.missingRatio ∅ l = 1

theorem Wallace.BlockSystem.missingRatio_mono (B : BlockSystem) {A C : Set ℕ} (hAC : A ⊆ C) (l : ℕ) : B.missingRatio C l ≤ B.missingRatio A l

theorem Wallace.BlockSystem.missingRatio_inter_le (B : BlockSystem) (A C : Set ℕ) (l : ℕ) : B.missingRatio (A ∩ C) l ≤ B.missingRatio A l + B.missingRatio C l

def Wallace.BlockSystem.IsLarge (B : BlockSystem) (a A : Set ℕ) : Prop

Sets having block density one along the labels in a.

Equations

• B.IsLarge a A = Filter.Tendsto (B.missingRatio A) (Filter.atTop ⊓ Filter.principal a) (nhds 0)

def Wallace.BlockSystem.densityFilter (B : BlockSystem) (a : Set ℕ) : Filter ℕ

The block-density-one sets form a filter.

Equations

• B.densityFilter a = { sets := {A : Set ℕ | B.IsLarge a A}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

@[simp]

theorem Wallace.BlockSystem.mem_densityFilter_iff (B : BlockSystem) (a A : Set ℕ) : A ∈ B.densityFilter a ↔ B.IsLarge a A

theorem Wallace.BlockSystem.densityFilter_le_cofinite (B : BlockSystem) (a : Set ℕ) : B.densityFilter a ≤ Filter.cofinite

Every cofinite set has block density one. In mathlib's reverse-inclusion order on filters, this says that the density filter lies below the cofinite filter.

theorem Wallace.BlockSystem.densityFilter_neBot (B : BlockSystem) {a : Set ℕ} (ha : a.Infinite) : (B.densityFilter a).NeBot

If the label set is infinite, the block-density filter is proper.

theorem Wallace.BlockSystem.exists_free_ultrafilter_le_densityFilter (B : BlockSystem) {a : Set ℕ} (ha : a.Infinite) : ∃ (p : Ultrafilter ℕ), ↑p ≤ B.densityFilter a ∧ ↑p ≤ Filter.cofinite

The density filter along an infinite almost-disjoint label set has a free ultrafilter extension. Both refinement inequalities are recorded explicitly.

Coefficient-independent block labels and ultrafilters

noncomputable def Wallace.BlockData.continuumIndexEquivBinaryStream : TriangularPreprocess.ContinuumIndex ≃ (ℕ → Bool)

A fixed identification of the canonical continuum index with binary streams.

Equations

• Wallace.BlockData.continuumIndexEquivBinaryStream = Classical.choice Wallace.BlockData.continuumIndexEquivBinaryStream._proof_1

def Wallace.BlockData.label (a : TriangularPreprocess.ContinuumIndex) : Set ℕ

The almost-disjoint block label assigned to a sequence code.

Equations

• Wallace.BlockData.label a = Wallace.binaryBranchOnNat (Wallace.BlockData.continuumIndexEquivBinaryStream a)

theorem Wallace.BlockData.label_infinite (a : TriangularPreprocess.ContinuumIndex) : (label a).Infinite

theorem Wallace.BlockData.label_inter_finite {a b : TriangularPreprocess.ContinuumIndex} (hab : a ≠ b) : (label a ∩ label b).Finite

@[reducible, inline]

abbrev Wallace.BlockData.blocks (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) : BlockSystem

The block system with the prescribed sizes.

Equations

• Wallace.BlockData.blocks N hN = Wallace.BlockSystem.ofBlockPositions N hN

noncomputable def Wallace.BlockData.ultrafilter (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (a : TriangularPreprocess.ContinuumIndex) : Ultrafilter ℕ

A free ultrafilter refining the density filter of a code's label.

Equations

• Wallace.BlockData.ultrafilter N hN a = Classical.choose ⋯

theorem Wallace.BlockData.ultrafilter_le_density (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (a : TriangularPreprocess.ContinuumIndex) : ↑(ultrafilter N hN a) ≤ (blocks N hN).densityFilter (label a)

theorem Wallace.BlockData.ultrafilter_free (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (a : TriangularPreprocess.ContinuumIndex) : ↑(ultrafilter N hN a) ≤ Filter.cofinite

def Wallace.AlmostDisjoint.earlierUnion {ι : Type u_1} {α : Type u_2} [Preorder ι] (family : ι → Set α) (j : ι) : Set α

The union of the members that occur strictly before j in an enumeration.

Equations

• Wallace.AlmostDisjoint.earlierUnion family j = ⋃ i ∈ Set.Iio j, family i

def Wallace.AlmostDisjoint.disjointize {ι : Type u_1} {α : Type u_2} [Preorder ι] (family : ι → Set α) (j : ι) : Set α

The standard recursive disjointization from the paper: b_j = a_j \ \bigcup_{i<j} a_i.

Equations

• Wallace.AlmostDisjoint.disjointize family j = family j \ Wallace.AlmostDisjoint.earlierUnion family j

theorem Wallace.AlmostDisjoint.disjointize_subset {ι : Type u_1} {α : Type u_2} [Preorder ι] (family : ι → Set α) (j : ι) : disjointize family j ⊆ family j

theorem Wallace.AlmostDisjoint.pairwise_disjoint_disjointize {ι : Type u_1} {α : Type u_2} [LinearOrder ι] (family : ι → Set α) : Pairwise fun (i j : ι) => Disjoint (disjointize family i) (disjointize family j)

Disjointization makes any linearly enumerated family pairwise disjoint; no almost-disjointness assumption is needed for this part.

theorem Wallace.AlmostDisjoint.disjointize_loss_finite {ι : Type u_1} {α : Type u_2} [LinearOrder ι] (family : ι → Set α) (had : Pairwise fun (i j : ι) => (family i ∩ family j).Finite) (j : ι) (hpred : (Set.Iio j).Finite) : (family j \ disjointize family j).Finite

If a_j has finite intersection with every predecessor and j has only finitely many predecessors, then the disjointization removes only finitely many points.

def Wallace.BlockSystem.retainedBlocks (B : BlockSystem) (b : Set ℕ) (E : ℕ → Finset ℕ) : Set ℕ

The points retained after deleting E l from every block whose label belongs to b. This is exactly the set U_α in equation (retained) of the paper.

Equations

• B.retainedBlocks b E = ⋃ l ∈ b, ↑(B.block l \ E l)

theorem Wallace.BlockSystem.missingRatio_retainedBlocks_le (B : BlockSystem) (b : Set ℕ) (E : ℕ → Finset ℕ) {l : ℕ} (hlb : l ∈ b) : B.missingRatio (B.retainedBlocks b E) l ≤ ↑(E l).card / ↑(B.block l).card

On a retained label, every point missing from the retained union lies in the corresponding deletion set.

theorem Wallace.BlockSystem.missingRatio_retainedBlocks_le_bound (B : BlockSystem) (b : Set ℕ) (E : ℕ → Finset ℕ) (R : ℕ → ℕ) {l : ℕ} (hlb : l ∈ b) (hcard : (E l).card ≤ R l) : B.missingRatio (B.retainedBlocks b E) l ≤ ↑(R l) / ↑(B.block l).card

The paper's quantitative estimate deficit ≤ R_l / card(block_l).

theorem Wallace.BlockSystem.retainedBlocks_mem_densityFilter (B : BlockSystem) {a b : Set ℕ} (E : ℕ → Finset ℕ) (R : ℕ → ℕ) (hab : (a \ b).Finite) (hcard : ∀ l ∈ b, (E l).card ≤ R l) (hratio : Filter.Tendsto (fun (l : ℕ) => ↑(R l) / ↑(B.block l).card) Filter.atTop (nhds 0)) : B.retainedBlocks b E ∈ B.densityFilter a

Bounded block deletions with vanishing relative bound are retained by the density filter. The hypothesis a \ b finite records b =* a together with b ⊆ a, which is the precise direction needed for the limit along a.

theorem Wallace.BlockSystem.retainedBlocks_mem_densityFilter_ofBlockPositions (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) {a b : Set ℕ} (E : ℕ → Finset ℕ) (R : ℕ → ℕ) (hab : (a \ b).Finite) (hcard : ∀ l ∈ b, (E l).card ≤ R l) (hratio : Filter.Tendsto (fun (l : ℕ) => ↑(R l) / ↑(N l)) Filter.atTop (nhds 0)) : (ofBlockPositions N hN).retainedBlocks b E ∈ (ofBlockPositions N hN).densityFilter a

Concrete specialization to the triangular preprocessing blocks. The denominator is now the prescribed paper size N l, by blockPositions_card.