OAI/Combinatorics/IndependentSets/Repetition/CoordinateCompletion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Repetition.CompletedSampling.coordinateLeft line 16
  2. def OAI.IndependentSetsGames.Foundations.Repetition.CompletedSampling.coordinateRight line 20
  3. theorem OAI.IndependentSetsGames.Foundations.Repetition.CompletedSampling.coordinateLeft_preserves line 26
  4. theorem OAI.IndependentSetsGames.Foundations.Repetition.CompletedSampling.coordinateRight_preserves line 33
  5. def OAI.IndependentSetsGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw line 38
  6. theorem OAI.IndependentSetsGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_mixture line 46
  7. theorem OAI.IndependentSetsGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_outputLaw line 81
  8. theorem OAI.IndependentSetsGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_totalVariation_le line 91
  9. def OAI.IndependentSetsGames.Foundations.Games.Game.localEmbeddingLaw line 114
  10. theorem OAI.IndependentSetsGames.Foundations.Games.Game.success_le_value_add_embedding_distance line 121
  11. def OAI.IndependentSetsGames.Foundations.Games.Game.coordinateGame line 150
  12. theorem OAI.IndependentSetsGames.Foundations.Games.Game.coordinate_probability_le_value_add_embedding_distance line 156
  13. theorem OAI.IndependentSetsGames.Foundations.Games.Game.coordinate_probability_le_value_of_approximate_embeddings line 171