BlockNoiseProbabilityLemmas.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Exact rational expectation for the quadratic block's conditioned noise.

abbrev OAI.UniqueGamesTheorem.Quadratic.NonzeroBlock line 23
Source documentation
The uniform noise space after conditioning the perturbation to be nonzero.
```
abbrev NonzeroBlock (v : Vec F) := {u : U v // u ≠ 0}
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.U
def OAI.UniqueGamesTheorem.Quadratic.nonzeroBlockChangeProbability line 26
Source documentation
Exact uniform expectation of the nonlinear-change indicator.
```
def nonzeroBlockChangeProbability (v : Vec F) (p : Vec F × Vec F) : ℚ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec
def OAI.UniqueGamesTheorem.Quadratic.conditionedChangedEquiv line 33
Source documentation
The zero perturbation is never a changed perturbation, so conditioning does not remove any element from the change event.
```
def conditionedChangedEquiv (v : Vec F) (p : Vec F × Vec F) :
    {u : NonzeroBlock v //
      blockObservable (p + (u.val : Vec F × Vec F)) ≠ blockObservable p} ≃
    {u : U v // blockObservable (p + (u : Vec F × Vec F)) ≠ blockObservable p} where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.NonzeroBlock, OAI.UniqueGamesTheorem.Quadratic.blockObservable, OAI.UniqueGamesTheorem.Quadratic.U
theorem OAI.UniqueGamesTheorem.Quadratic.nonzeroBlockChangeProbability_eq_count line 42
theorem OAI.UniqueGamesTheorem.Quadratic.nonzeroBlockChangeProbability_eq line 60
Source documentation
The one-level change probability is exactly 1-θ, for every fixed input. Here θ = 1/(q²+q+1) and q is the actual finite-field cardinality.
```
theorem nonzeroBlockChangeProbability_eq (v : Vec F) (hv : v ≠ 0)
    (p : Vec F × Vec F) :
    nonzeroBlockChangeProbability v p =
      1 - 1 / ((Nat.card F : ℚ) ^ 2 + (Nat.card F : ℚ) + 1) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.nonzeroBlockChangeProbability
abbrev OAI.UniqueGamesTheorem.Quadratic.BlockOrientation line 89
Source documentation
An orientation identifies the common binary alphabet with a line's block.
```
abbrev BlockOrientation (A : FieldLine F) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.FieldLine
instance OAI.UniqueGamesTheorem.Quadratic.fieldLineFintype line 92
instance OAI.UniqueGamesTheorem.Quadratic.finiteBlockOrientation line 94
instance OAI.UniqueGamesTheorem.Quadratic.blockOrientationFintype line 97
def OAI.UniqueGamesTheorem.Quadratic.chosenBlockOrientation line 101
Source documentation
Existence uses the proved dimension of the actual quadratic block.
```
noncomputable def chosenBlockOrientation (A : FieldLine F) : BlockOrientation A :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.BlockOrientation
def OAI.UniqueGamesTheorem.Quadratic.blockOrientationEquiv line 107
Source documentation
Composing with one fixed orientation identifies all orientations with automorphisms of the common binary alphabet.
```
noncomputable def blockOrientationEquiv (A : FieldLine F) :
    BlockOrientation A ≃ (Vec F ≃ₗ[ZMod 2] Vec F) where
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.BlockOrientation, OAI.UniqueGamesTheorem.Quadratic.Vec
theorem OAI.UniqueGamesTheorem.Quadratic.card_blockOrientation line 120
theorem OAI.UniqueGamesTheorem.Quadratic.card_blockOrientation_eq line 124
theorem OAI.UniqueGamesTheorem.Quadratic.card_blockOrientation_pos line 128
abbrev OAI.UniqueGamesTheorem.Quadratic.BlockOrientationIndex line 133
def OAI.UniqueGamesTheorem.Quadratic.blockOrientationIndexEquiv line 136
theorem OAI.UniqueGamesTheorem.Quadratic.card_blockOrientationIndex line 147