OAI/Combinatorics/BalancedRyser/Probability/PatternGate.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.PatternModel.gated line 11
  2. theorem OAI.Balanced.PatternModel.gated_measure line 30
  3. theorem OAI.Balanced.PatternModel.gated_fixCoordinates line 32
  4. theorem OAI.Balanced.PatternModel.gated_fixedExpectation line 35
  5. theorem OAI.Balanced.PatternModel.gated_support_card_le line 39
  6. theorem OAI.Balanced.PatternModel.gated_indicator line 43
  7. theorem OAI.Balanced.PatternModel.gated_count line 47
  8. theorem OAI.Balanced.PatternModel.gated_overlapCount line 53
  9. theorem OAI.Balanced.PatternModel.gate_fixed_iff line 68
  10. theorem OAI.Balanced.PatternModel.fixedExpectation_gated_function line 74
  11. theorem OAI.Balanced.PatternModel.gated_fixed_count line 91
  12. theorem OAI.Balanced.PatternModel.gated_fixed_overlapCount line 101
  13. theorem OAI.Balanced.PatternModel.gated_centered_moment_le line 113