Concrete triangular data for the rational direct sum

This module chooses, uniformly for every coded injective rational sequence, its prepared subsequence and its free block-density ultrafilter.

noncomputable def Wallace.RationalData.selector (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : RationalTriangularPreprocess.ContinuumIndex) : ℕ → ℕ

Strictly increasing selector supplied by rational block preprocessing.

Equations

• Wallace.RationalData.selector N hN M a = Classical.choose ⋯

theorem Wallace.RationalData.selector_strictMono (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : RationalTriangularPreprocess.ContinuumIndex) : StrictMono (selector N hN M a)

noncomputable def Wallace.RationalData.prepared (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : RationalTriangularPreprocess.ContinuumIndex) (n : ℕ) : RationalTriangularPreprocess.ContinuumRationalGroup

Prepared subsequence represented by code a.

Equations

• Wallace.RationalData.prepared N hN M a n = Wallace.RationalTriangularPreprocess.codedSequence a (Wallace.RationalData.selector N hN M a n)

noncomputable def Wallace.RationalData.differenceBlock (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : RationalTriangularPreprocess.ContinuumIndex) (l : ℕ) : Finset RationalTriangularPreprocess.ContinuumRationalGroup

Shifted finite set in block l.

Equations

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

theorem Wallace.RationalData.differenceBlock_boundedIndependent (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : RationalTriangularPreprocess.ContinuumIndex) (l : ℕ) : FiniteCombinatorics.BoundedIndependent (M l) (differenceBlock N hN M a l)

theorem Wallace.RationalData.prepared_support_lt (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : RationalTriangularPreprocess.ContinuumIndex) (n : ℕ) (i : RationalTriangularPreprocess.ContinuumIndex) (hi : i ∈ (prepared N hN M a n).support) : i < RationalTriangularPreprocess.codeIndex a

theorem Wallace.RationalData.prepared_injective (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : RationalTriangularPreprocess.ContinuumIndex) : Function.Injective (prepared N hN M a)

theorem Wallace.RationalData.preparedDifference_injective (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : RationalTriangularPreprocess.ContinuumIndex) : Function.Injective fun (n : ℕ) => prepared N hN M a n - RationalTriangularPreprocess.codeBasisVector a

noncomputable def Wallace.RationalData.transfiniteData (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) : RationalTransfiniteExtension.ContinuumData

Concrete input for the rational transfinite recursion.

Equations

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