OAI/Combinatorics/FiniteCircle/MaskBranching.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.few_large_prime_divisors line 11
  2. theorem OAI.FiniteCircle.many_mask_children line 39
  3. def OAI.FiniteCircle.FrequencyTree line 69
  4. def OAI.FiniteCircle.frequencySum line 73
  5. def OAI.FiniteCircle.frequencyMass line 78
  6. theorem OAI.FiniteCircle.frequencySum_natAbs_le_mass line 83
  7. def OAI.FiniteCircle.MaskChildren line 91
  8. instance OAI.FiniteCircle.maskChildrenFintype line 93
  9. def OAI.FiniteCircle.MaskCongruences line 96
  10. theorem OAI.FiniteCircle.mask_branching_induction line 104
  11. theorem OAI.FiniteCircle.mask_frequency_branching line 150