OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Surviving.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryFrequencyChain.surviving line 25
  2. def OAI.OrdinaryFrequencyChain.firstGood line 29
  3. lemma OAI.OrdinaryFrequencyChain.surviving_zero line 34
  4. lemma OAI.OrdinaryFrequencyChain.surviving_succ line 41
  5. lemma OAI.OrdinaryFrequencyChain.sum_partition line 55
  6. lemma OAI.OrdinaryFrequencyChain.square_two line 66
  7. lemma OAI.OrdinaryFrequencyChain.approximation_energy line 71
  8. theorem OAI.OrdinaryFrequencyChain.first_good_energy line 84
  9. lemma OAI.OrdinaryFrequencyChain.binned_energy line 103
  10. lemma OAI.OrdinaryFrequencyChain.sum_filter_exists_le line 115
  11. def OAI.OrdinaryFrequencyChain.allBinsGood line 131
  12. theorem OAI.OrdinaryFrequencyChain.next_stage_energy line 134
  13. lemma OAI.OrdinaryFrequencyChain.sparse_union line 159