Disjointizing a countable almost-disjoint family

The block fusion uses a countable subfamily of the fixed almost-disjoint family. This module orders any countable index type by an injection into ℕ and applies the standard predecessor deletion. Each label loses only finitely many points.

theorem Wallace.exists_disjoint_refinement_countable {ι : Type u} {α : Type v} [Countable ι] (family : ι → Set α) (had : Pairwise fun (i j : ι) => (family i ∩ family j).Finite) : ∃ (refined : ι → Set α), (Pairwise fun (i j : ι) => Disjoint (refined i) (refined j)) ∧ ∀ (i : ι), refined i ⊆ family i ∧ (family i \ refined i).Finite

Every countable almost-disjoint family has a pairwise disjoint refinement modulo finite sets. Unlike an enumeration by a surjection, this statement also handles finite and empty index types without duplicate indices.

Scheduling the relevant Wallace codes

@[reducible, inline]

abbrev Wallace.LocalCodeSchedule.RelevantCode (index : TriangularPreprocess.ContinuumIndex ↪ TriangularPreprocess.ContinuumIndex) (D : Set TriangularPreprocess.ContinuumIndex) : Type

Codes whose distinguished coordinate belongs to a given coordinate set.

Equations

• Wallace.LocalCodeSchedule.RelevantCode index D = { a : Wallace.TriangularPreprocess.ContinuumIndex // index a ∈ D }

def Wallace.LocalCodeSchedule.refinedLabel (index : TriangularPreprocess.ContinuumIndex ↪ TriangularPreprocess.ContinuumIndex) (D : Set TriangularPreprocess.ContinuumIndex) (hD : D.Countable) : RelevantCode index D → Set ℕ

Pairwise-disjoint refinements of the labels of all codes relevant to D.

Equations

• Wallace.LocalCodeSchedule.refinedLabel index D hD = Classical.choose ⋯

theorem Wallace.LocalCodeSchedule.refinedLabel_pairwise (index : TriangularPreprocess.ContinuumIndex ↪ TriangularPreprocess.ContinuumIndex) (D : Set TriangularPreprocess.ContinuumIndex) (hD : D.Countable) : Pairwise fun (a b : RelevantCode index D) => Disjoint (refinedLabel index D hD a) (refinedLabel index D hD b)

theorem Wallace.LocalCodeSchedule.label_diff_refinedLabel_finite (index : TriangularPreprocess.ContinuumIndex ↪ TriangularPreprocess.ContinuumIndex) (D : Set TriangularPreprocess.ContinuumIndex) (hD : D.Countable) (a : RelevantCode index D) : (BlockData.label ↑a \ refinedLabel index D hD a).Finite

noncomputable def Wallace.LocalCodeSchedule.activeCode (index : TriangularPreprocess.ContinuumIndex ↪ TriangularPreprocess.ContinuumIndex) (D : Set TriangularPreprocess.ContinuumIndex) (hD : D.Countable) (l : ℕ) : Option (RelevantCode index D)

The unique relevant code scheduled at a label, when one exists.

Equations

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

theorem Wallace.LocalCodeSchedule.activeCode_eq_some_of_mem (index : TriangularPreprocess.ContinuumIndex ↪ TriangularPreprocess.ContinuumIndex) (D : Set TriangularPreprocess.ContinuumIndex) (hD : D.Countable) (l : ℕ) (a : RelevantCode index D) (ha : l ∈ refinedLabel index D hD a) : activeCode index D hD l = some a