OAI/Combinatorics/TreeEdit/SampledSpectrum.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TreeEdit.TorusFourier.high line 9
2. def OAI.TreeEdit.TorusFourier.highMass line 12
3. lemma OAI.TreeEdit.TorusFourier.high_nonneg line 15
4. lemma OAI.TreeEdit.TorusFourier.active_summary line 18
5. lemma OAI.TreeEdit.TorusFourier.branch_multiplier line 24
6. lemma OAI.TreeEdit.TorusFourier.branch_mass line 70
7. def OAI.TreeEdit.TorusFourier.SpectralBound line 86
8. lemma OAI.TreeEdit.TorusFourier.SpectralBound.child line 92
9. lemma OAI.TreeEdit.TorusFourier.high_estimate line 102
10. lemma OAI.TreeEdit.TorusFourier.cycle_estimate line 140
11. lemma OAI.TreeEdit.TorusFourier.mass_bound line 185
12. lemma OAI.TreeEdit.TorusFourier.energy_diagonal_le_mass line 256
13. theorem OAI.TreeEdit.TorusFourier.displacement_bound line 274