OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/EnergyLeGram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryLogDifferencing.energy_le_gram line 12
2. lemma OAI.OrdinaryLogDifferencing.norm_sum_sq line 32
3. lemma OAI.OrdinaryLogDifferencing.shift_difference line 40
4. lemma OAI.OrdinaryLogDifferencing.norm_shift_difference line 49
5. lemma OAI.OrdinaryLogDifferencing.shift_average_error line 60
6. theorem OAI.OrdinaryLogDifferencing.finite_differencing line 79
7. theorem OAI.OrdinaryLogDifferencing.row_gap_sum line 106
8. theorem OAI.OrdinaryLogDifferencing.correlation_envelope line 155