OAI/Computability/UniqueGames/Soundness/ConditionalSimulationLemmas.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual local simulation in Lemma 6.8 after fixing H. These reconstruction maps consume only the first player's occurrence tuple or the second player's name tuple. Its winning-event containment is proved from the concrete equation and named-projection predicates.

  1. instance OAI.UniqueGamesTheorem.Soundness.ConditionalSimulation.firstInputFintype line 24
  2. instance OAI.UniqueGamesTheorem.Soundness.ConditionalSimulation.secondInputFintype line 33
  3. def OAI.UniqueGamesTheorem.Soundness.ConditionalSimulation.incidenceGame line 43
  4. def OAI.UniqueGamesTheorem.Soundness.ConditionalSimulation.actualLocalSimulation line 48
  5. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalSimulation.actual_conditioned_strategy_success_le_repeated_value line 86
  6. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.uniform_probability_decide line 127
  7. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.OuterStrategy line 145
  8. def OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.actualWin line 149
  9. def OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.conditionedWinProbability line 155
  10. def OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.reconstructedEvent line 165
  11. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.actualWin_iff_reconstructedEvent line 177
  12. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.conditionedWinProbability_eq_fresh line 194
  13. def OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.incidenceLaw line 216
  14. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.reconstructed_success_eq_fresh_average line 219
  15. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.conditioned_probability_le_repeated_value line 256

    Source documentation

    The actual finite observation-fibre probability is bounded by the genuine repeated incidence-game value. The sampling identity is proved internally.

    theorem conditioned_probability_le_repeated_value [Nonempty O]
    (J : Finset P) (g : Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (observed : PositionOutside (zeroSet J gamma) → O × N)
    (reference : RawObservationFibre J g.name gamma observed)
    (e : Fin (zeroSet J gamma).card ≃ PositionInside (zeroSet J gamma))
    (strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N))
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.ConditionalGameLaw.OuterStrategy