OAI/NumberTheory/Ostmann/Construction/HarmonicMatchedEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The matched diagonal bound for the actual harmonic tuple laws

  1. theorem OAI.Ostmann.harmonic_tuple_point_of_window line 12
  2. theorem OAI.Ostmann.harmonic_matched_diagonal_energy line 21