The countable block schedule around one rational vector

Relevant codes are countable. Their almost-disjoint labels are disjointized, so every block has at most one active code, and its shifted prepared terms form the finite independent set used by the fusion.

@[reducible, inline]

abbrev Wallace.RationalLocalSetup.RelevantCode (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) : Type

Codes whose distinguished coordinate lies in the local closure of x.

Equations

• Wallace.RationalLocalSetup.RelevantCode N hN M x = Wallace.LocalCodeSchedule.RelevantCode Wallace.RationalTriangularPreprocess.codeIndex (Wallace.RationalClosure.closure N hN M x)

def Wallace.RationalLocalSetup.refinedLabel (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) : RelevantCode N hN M x → Set ℕ

Pairwise-disjoint refinements of the block labels of all relevant codes.

Equations

• Wallace.RationalLocalSetup.refinedLabel N hN M x = Wallace.LocalCodeSchedule.refinedLabel Wallace.RationalTriangularPreprocess.codeIndex (Wallace.RationalClosure.closure N hN M x) ⋯

theorem Wallace.RationalLocalSetup.label_diff_refinedLabel_finite (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RelevantCode N hN M x) : (BlockData.label ↑a \ refinedLabel N hN M x a).Finite

noncomputable def Wallace.RationalLocalSetup.activeCode (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (l : ℕ) : Option (RelevantCode N hN M x)

The unique relevant code assigned to stage l, when one exists.

Equations

• Wallace.RationalLocalSetup.activeCode N hN M x l = Wallace.LocalCodeSchedule.activeCode Wallace.RationalTriangularPreprocess.codeIndex (Wallace.RationalClosure.closure N hN M x) ⋯ l

theorem Wallace.RationalLocalSetup.activeCode_eq_some_of_mem (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (l : ℕ) (a : RelevantCode N hN M x) (ha : l ∈ refinedLabel N hN M x a) : activeCode N hN M x l = some a

The countable local rational group

noncomputable def Wallace.RationalLocalSetup.closureInclusion (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) : (↑(RationalClosure.closure N hN M x) →₀ ℚ) →+ RationalTriangularPreprocess.ContinuumRationalGroup

The additive inclusion of the local rational direct sum into the ambient one.

Equations

• Wallace.RationalLocalSetup.closureInclusion N hN M x = Finsupp.embDomain.addMonoidHom (Function.Embedding.subtype (Wallace.RationalClosure.closure N hN M x))

theorem Wallace.RationalLocalSetup.closureInclusion_apply (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (z : ↑(RationalClosure.closure N hN M x) →₀ ℚ) : (closureInclusion N hN M x) z = Finsupp.embDomain (Function.Embedding.subtype (RationalClosure.closure N hN M x)) z

theorem Wallace.RationalLocalSetup.closureInclusion_injective (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) : Function.Injective ⇑(closureInclusion N hN M x)

noncomputable def Wallace.RationalLocalSetup.localDifference (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RelevantCode N hN M x) (n : ℕ) : ↑(RationalClosure.closure N hN M x) →₀ ℚ

The prepared difference restricted to the local coordinate closure.

Equations

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

theorem Wallace.RationalLocalSetup.closureInclusion_localDifference (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RelevantCode N hN M x) (n : ℕ) : (closureInclusion N hN M x) (localDifference N hN M x a n) = RationalData.prepared N hN M (↑a) n - RationalTriangularPreprocess.codeBasisVector ↑a

theorem Wallace.RationalLocalSetup.localDifference_injective (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RelevantCode N hN M x) : Function.Injective (localDifference N hN M x a)

noncomputable def Wallace.RationalLocalSetup.localDifferenceBlock (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RelevantCode N hN M x) (l : ℕ) : Finset (↑(RationalClosure.closure N hN M x) →₀ ℚ)

The finite block of local prepared differences for a relevant code.

Equations

• Wallace.RationalLocalSetup.localDifferenceBlock N hN M x a l = Finset.image (Wallace.RationalLocalSetup.localDifference N hN M x a) (Wallace.TriangularPreprocess.blockPositions N hN l)

theorem Wallace.RationalLocalSetup.localDifferenceBlock_card (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RelevantCode N hN M x) (l : ℕ) : (localDifferenceBlock N hN M x a l).card = N l

theorem Wallace.RationalLocalSetup.localDifferenceBlock_image_inclusion (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RelevantCode N hN M x) (l : ℕ) : Finset.image (⇑(closureInclusion N hN M x)) (localDifferenceBlock N hN M x a l) = RationalData.differenceBlock N hN M (↑a) l

theorem Wallace.RationalLocalSetup.localDifferenceBlock_boundedIndependent (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RelevantCode N hN M x) (l : ℕ) : FiniteCombinatorics.BoundedIndependent (M l) (localDifferenceBlock N hN M x a l)

noncomputable def Wallace.RationalLocalSetup.localActiveBlock (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (l : ℕ) : Finset (↑(RationalClosure.closure N hN M x) →₀ ℚ)

The local difference block active at stage l, or the empty block.

Equations

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

theorem Wallace.RationalLocalSetup.localActiveBlock_eq_of_mem (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (l : ℕ) (a : RelevantCode N hN M x) (ha : l ∈ refinedLabel N hN M x a) : localActiveBlock N hN M x l = localDifferenceBlock N hN M x a l

theorem Wallace.RationalLocalSetup.localActiveBlock_boundedIndependent (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (l : ℕ) : FiniteCombinatorics.BoundedIndependent (M l) (localActiveBlock N hN M x l)

theorem Wallace.RationalLocalSetup.localActiveBlock_card_le (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (l : ℕ) : (localActiveBlock N hN M x l).card ≤ N l