HarmonicLoss.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Harmonic loss for the actual quadratic child maps

The probabilistic hypotheses of the harmonic accounting lemmas are discharged here by the proved field-line kernel criterion and genericity count.

theorem OAI.UniqueGamesTheorem.Quadratic.exists_nonzero_kernel_of_range_rank_lt line 23
theorem OAI.UniqueGamesTheorem.Quadratic.probability_rank_drop_le_loss_count line 40
def OAI.UniqueGamesTheorem.Quadratic.fieldLineTheta line 67
theorem OAI.UniqueGamesTheorem.Quadratic.fieldLineTheta_eq line 71
def OAI.UniqueGamesTheorem.Quadratic.nextBlockRank line 76
Source documentation
The image dimension of the actual oriented child restriction map.
```
def nextBlockRank (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (J : ∀ A : FieldLine F, BlockOrientation A)
    (A : FieldLine F) : ℕ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.BlockOrientation
theorem OAI.UniqueGamesTheorem.Quadratic.nextBlockRank_le line 81
theorem OAI.UniqueGamesTheorem.Quadratic.nextBlockRank_independent line 87
Source documentation
Changing the binary orientation of every child leaves its logical image rank unchanged.
```
theorem nextBlockRank_independent (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (J J' : ∀ A : FieldLine F, BlockOrientation A)
    (A : FieldLine F) : nextBlockRank S g J A = nextBlockRank S g J' A := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.BlockOrientation, OAI.UniqueGamesTheorem.Quadratic.nextBlockRank
theorem OAI.UniqueGamesTheorem.Quadratic.generic_nextBlockRank_dichotomy line 99
theorem OAI.UniqueGamesTheorem.Quadratic.generic_block_loss_probability_le line 111
theorem OAI.UniqueGamesTheorem.Quadratic.generic_block_harmonic_loss_le line 127
Source documentation
Actual generic block restrictions have rank-independent expected harmonic loss.
```
theorem generic_block_harmonic_loss_le (S : Submodule (ZMod 2) (Vec F))
    (g : S →ₗ[ZMod 2] Vec F) (J : ∀ A : FieldLine F, BlockOrientation A)
    (hS : IsGeneric S) :
    average (fun A => harmonic (Module.finrank (ZMod 2) S) -
      harmonic (nextBlockRank S g J A)) ≤ 3 * fieldLineTheta F := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.Vec, OAI.UniqueGamesTheorem.Quadratic.FieldLine, OAI.UniqueGamesTheorem.Quadratic.BlockOrientation, OAI.UniqueGamesTheorem.Quadratic.IsGeneric, OAI.UniqueGamesTheorem.Quadratic.nextBlockRank, OAI.UniqueGamesTheorem.Quadratic.fieldLineTheta
theorem OAI.UniqueGamesTheorem.Quadratic.card_loss_fieldLineRestrictions_le_nonzero line 149
theorem OAI.UniqueGamesTheorem.Quadratic.arbitrary_block_loss_probability_le line 164
theorem OAI.UniqueGamesTheorem.Quadratic.arbitrary_block_harmonic_loss_le line 184