OAI/Combinatorics/IndependentSets/Expansion/PoweringLazy.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.lazyRotate line 12
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.lazyRotate_involutive line 16
  3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.lazyGraph line 24
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_false line 32
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_true line 35
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLazy.operator_binomialMean line 46
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLazy.averagingOperator_lazy line 54
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLazy.iterate_lazy_eq_binomialMean line 66
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLazy.iterate_mem_Icc line 80
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLazy.lazy_endpoint_modal_transfer line 95
  11. def OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.constraintGraph line 114
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.constraintGraph_tail line 126
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.constraintGraph_reverse line 129
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.constraintGraph_portGraph line 132
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.edgeSatisfied_false line 136
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.edgeSatisfied_true line 140
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.complete line 149
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.complete_iff line 159
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.satisfiable_iff line 170
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.rejectionCount_eq line 178
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.card_ports line 187
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.card_darts line 191
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.LazyConstraint.rejection_density_eq_half line 195