GameDecoder.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Weighted question averaging and the actual finite-game consequence of the Håstad decoder. The game value is the maximum over deterministic private answer tables; the Fourier responses are derandomized by the checked table law.

theorem OAI.MaxCutGames.Foundations.Hastad.distribution_sq_expectation_le line 17
def OAI.MaxCutGames.Foundations.Hastad.projectionGame line 47
def OAI.MaxCutGames.Foundations.Hastad.questionBias line 52
def OAI.MaxCutGames.Foundations.Hastad.questionAcceptance line 56
theorem OAI.MaxCutGames.Foundations.Hastad.questionAcceptance_eq line 61
inductive OAI.MaxCutGames.Foundations.Hastad.ConditionedOracle line 74
Source documentation
Storage distinguishes an actually empty legal domain from a folded table over its legal assignments. The empty case needs no nonexistent fold point.
```
inductive ConditionedOracle (valid : J → Bool) where
…
```
def OAI.MaxCutGames.Foundations.Hastad.ConditionedOracle.answer line 78
def OAI.MaxCutGames.Foundations.Hastad.ConditionedOracle.fallback line 82
theorem OAI.MaxCutGames.Foundations.Hastad.testBias_constant_right line 88
theorem OAI.MaxCutGames.Foundations.Hastad.empty_conditioned_bias line 95
theorem OAI.MaxCutGames.Foundations.Hastad.conditionedOracle_response_bound line 105
theorem OAI.MaxCutGames.Foundations.Hastad.folded_game_decoder_bound line 125

theorem OAI.MaxCutGames.Foundations.Hastad.conditionedOracle_game_decoder_bound line 165

Source documentation

The game bound includes inconsistent clause tuples, whose legal local domain is empty and whose implemented right oracle is constant.

theorem conditionedOracle_game_decoder_bound
    (questions : FiniteDistribution (Q₁ × Q₂))
    (ε : ℝ) (π : Q₁ → Q₂ → J → I) (valid : Q₂ → J → Bool)
    (i₀ : Q₁ → I) (tableA : ∀ q, HalfCube (i₀ q) → Bool)
    (default : J) (right : ∀ q, ConditionedOracle (valid q))
    (hε : 0 < ε) (hε' : ε ≤ 1 / 2) :
    4 * ε * questions.expectation (questionBias ε π
      (fun q => foldedAnswer (i₀ q) (tableA q)) (fun q => (right q).answer)) ^ 2 ≤
      (projectionGame questions π valid).value := by
…

Mentions: OAI.MaxCutGames.Foundations.Hastad.HalfCube, OAI.MaxCutGames.Foundations.Hastad.ConditionedOracle, OAI.MaxCutGames.Foundations.Hastad.questionBias, OAI.MaxCutGames.Foundations.Hastad.foldedAnswer, OAI.MaxCutGames.Foundations.Hastad.projectionGame

theorem OAI.MaxCutGames.Foundations.Hastad.conditionedOracle_acceptance_bound line 201