OAI/NumberTheory/Ostmann/Arithmetic/SingleFrequencyTree.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The frequency budget for one squared history

Unlike a pair of histories, this sum has exactly one frequency at each leaf. This is needed before the level-zero square-weight cancellation.

  1. def OAI.Ostmann.singleFrequencyKernel line 15
  2. def OAI.Ostmann.singleFrequencyLeaf line 19
  3. theorem OAI.Ostmann.signed_reducedFrequency_sum_le line 22
  4. theorem OAI.Ostmann.singleFrequencyKernel_sum_le line 38
  5. theorem OAI.Ostmann.singleFrequencyLeaf_sum_le line 62
  6. theorem OAI.Ostmann.single_frequency_tree_sum_le line 74
  7. def OAI.Ostmann.singleFrequencySplitList line 92
  8. theorem OAI.Ostmann.singleFrequencySplitList_length line 98
  9. def OAI.Ostmann.singleFrequencySupportBound line 108
  10. theorem OAI.Ostmann.singleFrequencyTreeWeight_eq line 111
  11. def OAI.Ostmann.singleTreeNodeFrequencies line 124
  12. theorem OAI.Ostmann.singleFrequencySplitList_modulus_mem line 128
  13. theorem OAI.Ostmann.singleTreeNodeFrequencies_divisor_bound line 142