Finite random restrictions

This file defines a completely finite sample space for sparse restrictions on exactly N variables. A symbol is either:

• one distinguished free symbol; or
• a Boolean value together with one of q copies.

Uniform sampling from Symbol q therefore leaves a coordinate free with probability 1 / (2 * q + 1) and fixes it to either Boolean value with probability q / (2 * q + 1). Retaining the copy label makes the distribution uniform on an honest finite type; no measure-theoretic or rational-probability convention is hidden in later counting arguments.

@[reducible, inline]

abbrev Complexity.RandomRestriction.Symbol (q : ℕ) : Type

One coordinate of the sparse-restriction sample space.

The left summand is the unique free symbol. The right summand fixes the coordinate and records one of q equiprobable copies of the chosen bit.

Equations

• Complexity.RandomRestriction.Symbol q = (Unit ⊕ Fin q × Bool)

@[reducible, inline]

abbrev Complexity.RandomRestriction.Seed (N q : ℕ) : Type

An independent sparse-restriction seed on exactly N variables.

Equations

• Complexity.RandomRestriction.Seed N q = (Fin N → Complexity.RandomRestriction.Symbol q)

def Complexity.RandomRestriction.decodeSymbol {q : ℕ} : Symbol q → Option Bool

Forget the multiplicity label and interpret a sample symbol as a partial Boolean assignment.

Equations

• Complexity.RandomRestriction.decodeSymbol (Sum.inl val) = none
• Complexity.RandomRestriction.decodeSymbol (Sum.inr (fst, value)) = some value

def Complexity.RandomRestriction.decode {N q : ℕ} (seed : Seed N q) : Restriction.On N

Decode a finite seed to the corresponding finite-arity restriction.

Equations

• Complexity.RandomRestriction.decode seed index = Complexity.RandomRestriction.decodeSymbol (seed index)

def Complexity.RandomRestriction.freeVariables {N q : ℕ} (seed : Seed N q) : Finset (Fin N)

The set of coordinates left free by a seed.

Equations

• Complexity.RandomRestriction.freeVariables seed = (Complexity.RandomRestriction.decode seed).freeVariables

def Complexity.RandomRestriction.eventCount {N : ℕ} (q : ℕ) (event : Restriction.On N → Prop) [DecidablePred event] : ℕ

The exact number of seeds whose decoded restriction satisfies event.

Equations

• Complexity.RandomRestriction.eventCount q event = {seed : Complexity.RandomRestriction.Seed N q | event (Complexity.RandomRestriction.decode seed)}.card

@[reducible, inline]

abbrev Complexity.RandomRestriction.EventSeed (N q : ℕ) (event : Restriction.On N → Prop) : Type

Seeds whose decoded restriction satisfies event. This subtype is the domain used by injective finite-encoding arguments.

Equations

• Complexity.RandomRestriction.EventSeed N q event = { seed : Complexity.RandomRestriction.Seed N q // event (Complexity.RandomRestriction.decode seed) }

noncomputable def Complexity.RandomRestriction.positionOf {s N : ℕ} (queries : Fin s ↪ Fin N) (index : Fin N) : Option (Fin s)

Locate an input coordinate in the range of an embedding.

Equations

• Complexity.RandomRestriction.positionOf queries index = if h : ∃ (position : Fin s), queries position = index then some (Classical.choose h) else none

noncomputable def Complexity.RandomRestriction.assignmentAlong {s N : ℕ} (queries : Fin s ↪ Fin N) (values : Fin s → Bool) : Restriction.On N

The finite partial assignment induced by embedded coordinates and their Boolean values.

Equations

• Complexity.RandomRestriction.assignmentAlong queries values index = Option.map values (Complexity.RandomRestriction.positionOf queries index)

noncomputable def Complexity.RandomRestriction.fixAlong {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (copies : Fin s → Fin q) (values : Fin s → Bool) : Seed N q

Replace the coordinates selected by queries by fixed symbols carrying the supplied copy labels and branch values.

Equations

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

noncomputable def Complexity.RandomRestriction.freeAlong {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) : Seed N q

Restore every coordinate selected by queries to the unique free symbol.

Equations

• Complexity.RandomRestriction.freeAlong seed queries index = match Complexity.RandomRestriction.positionOf queries index with | none => seed index | some val => Sum.inl ()