Finite random restrictions -- proof internals

theorem Complexity.RandomRestriction.card_seed_internal (N q : ℕ) : Fintype.card (Seed N q) = (2 * q + 1) ^ N

theorem Complexity.RandomRestriction.card_decodeSymbol_none_internal (q : ℕ) : {symbol : Symbol q | decodeSymbol symbol = none}.card = 1

theorem Complexity.RandomRestriction.eventCount_coordinate_free_internal {N : ℕ} (q : ℕ) (index : Fin N) : (eventCount q fun (restriction : Restriction.On N) => restriction index = none) = (2 * q + 1) ^ (N - 1)

Exactly (2q + 1)^(N - 1) seeds leave one prescribed coordinate free.

theorem Complexity.RandomRestriction.card_decodeSymbol_some_internal (q : ℕ) (value : Bool) : {symbol : Symbol q | decodeSymbol symbol = some value}.card = q

theorem Complexity.RandomRestriction.decodeSymbol_eq_none_iff_internal {q : ℕ} (symbol : Symbol q) : decodeSymbol symbol = none ↔ symbol = Sum.inl ()

theorem Complexity.RandomRestriction.eventCount_le_internal {N q : ℕ} (event : Restriction.On N → Prop) [DecidablePred event] : eventCount q event ≤ (2 * q + 1) ^ N

theorem Complexity.RandomRestriction.eventCount_true_internal (N q : ℕ) : (eventCount q fun (x : Restriction.On N) => True) = (2 * q + 1) ^ N

theorem Complexity.RandomRestriction.eventCount_congr_internal {N q : ℕ} (left right : Restriction.On N → Prop) [DecidablePred left] [DecidablePred right] (hiff : ∀ (restriction : Restriction.On N), left restriction ↔ right restriction) : eventCount q left = eventCount q right

theorem Complexity.RandomRestriction.eventCount_mono_internal {N q : ℕ} (left right : Restriction.On N → Prop) [DecidablePred left] [DecidablePred right] (himp : ∀ (restriction : Restriction.On N), left restriction → right restriction) : eventCount q left ≤ eventCount q right

theorem Complexity.RandomRestriction.eventCount_or_le_add_internal {N q : ℕ} (left right : Restriction.On N → Prop) [DecidablePred left] [DecidablePred right] : (eventCount q fun (restriction : Restriction.On N) => left restriction ∨ right restriction) ≤ eventCount q left + eventCount q right

theorem Complexity.RandomRestriction.eventCount_exists_le_sum_internal {N q : ℕ} {ι : Type} [Fintype ι] (event : ι → Restriction.On N → Prop) [(index : ι) → DecidablePred (event index)] : (eventCount q fun (restriction : Restriction.On N) => ∃ (index : ι), event index restriction) ≤ ∑ index : ι, eventCount q (event index)

theorem Complexity.RandomRestriction.card_eventSeed_internal {N q : ℕ} (event : Restriction.On N → Prop) [DecidablePred event] : Fintype.card (EventSeed N q event) = eventCount q event

theorem Complexity.RandomRestriction.eventCount_freeVariables_empty_internal (N q : ℕ) : (eventCount q fun (restriction : Restriction.On N) => restriction.freeVariables = ∅) = (2 * q) ^ N

theorem Complexity.RandomRestriction.eventCount_freeVariables_nonempty_internal (N q : ℕ) : (eventCount q fun (restriction : Restriction.On N) => restriction.freeVariables.Nonempty) = (2 * q + 1) ^ N - (2 * q) ^ N

theorem Complexity.RandomRestriction.eventCount_one_le_freeVariables_internal (N q : ℕ) : (eventCount q fun (restriction : Restriction.On N) => 1 ≤ restriction.freeVariables.card) = (2 * q + 1) ^ N - (2 * q) ^ N

theorem Complexity.RandomRestriction.eventCount_mul_pow_le_of_encoding_internal {N q : ℕ} (event : Restriction.On N → Prop) [DecidablePred event] (queryCount : ℕ) (Code : Type) [Fintype Code] (encode : EventSeed N q event × (Fin queryCount → Fin q) → Seed N q × Code) (injective : Function.Injective encode) : eventCount q event * q ^ queryCount ≤ (2 * q + 1) ^ N * Fintype.card Code

theorem Complexity.RandomRestriction.positionOf_apply_internal {s N : ℕ} (queries : Fin s ↪ Fin N) (position : Fin s) : positionOf queries (queries position) = some position

theorem Complexity.RandomRestriction.positionOf_eq_some_internal {s N : ℕ} (queries : Fin s ↪ Fin N) (index : Fin N) (position : Fin s) (hposition : positionOf queries index = some position) : queries position = index

theorem Complexity.RandomRestriction.assignmentAlong_disjoint_internal {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (values : Fin s → Bool) (free : ∀ (position : Fin s), decode seed (queries position) = none) (index : Fin N) : assignmentAlong queries values index = none ∨ decode seed index = none

theorem Complexity.RandomRestriction.assignmentAlong_apply_internal {s N : ℕ} (queries : Fin s ↪ Fin N) (values : Fin s → Bool) (position : Fin s) : assignmentAlong queries values (queries position) = some (values position)

theorem Complexity.RandomRestriction.decode_fixAlong_internal {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (copies : Fin s → Fin q) (values : Fin s → Bool) : decode (fixAlong seed queries copies values) = (assignmentAlong queries values).comp (decode seed)

theorem Complexity.RandomRestriction.fixAlong_apply_internal {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (copies : Fin s → Fin q) (values : Fin s → Bool) (position : Fin s) : fixAlong seed queries copies values (queries position) = Sum.inr (copies position, values position)

theorem Complexity.RandomRestriction.freeAlong_apply_internal {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (position : Fin s) : freeAlong seed queries (queries position) = Sum.inl ()

theorem Complexity.RandomRestriction.freeAlong_fixAlong_internal {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (copies : Fin s → Fin q) (values : Fin s → Bool) (free : ∀ (position : Fin s), seed (queries position) = Sum.inl ()) : freeAlong (fixAlong seed queries copies values) queries = seed

theorem Complexity.RandomRestriction.fixAlong_seed_copies_injective_internal {s N q : ℕ} (queries : Fin s ↪ Fin N) (values : Fin s → Bool) : Function.Injective fun (pair : { seed : Seed N q // ∀ (position : Fin s), seed (queries position) = Sum.inl () } × (Fin s → Fin q)) => fixAlong (↑pair.1) queries pair.2 values

theorem Complexity.RandomRestriction.mem_freeVariables_internal {N q : ℕ} (seed : Seed N q) (index : Fin N) : index ∈ freeVariables seed ↔ decode seed index = none