OAI/Analysis/NodalLength/GridPaths.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpNodal.Profiles.GridWord line 200
2. def OAI.SharpNodal.Profiles.wordIndex line 202
3. lemma OAI.SharpNodal.Profiles.wordIndex_injective line 207
4. def OAI.SharpNodal.Profiles.wordCenter line 220
5. lemma OAI.SharpNodal.Profiles.wordCenter_zero line 222
6. lemma OAI.SharpNodal.Profiles.wordCenter_succ line 226
7. lemma OAI.SharpNodal.Profiles.word_rescale_succ line 239
8. lemma OAI.SharpNodal.Profiles.gridWord_card line 248
9. lemma OAI.SharpNodal.Profiles.expect_word_succ line 252
10. def OAI.SharpNodal.Profiles.WaveTree.PathGood line 267
11. lemma OAI.SharpNodal.Profiles.WaveTree.expect_pathGood line 273
12. def OAI.SharpNodal.Profiles.HighWavePath line 297
13. lemma OAI.SharpNodal.Profiles.WaveTree.highPath_of_good line 303
14. theorem OAI.SharpNodal.Profiles.actual_path_stability line 316
15. lemma OAI.SharpNodal.Profiles.rescaleMap_mapsTo_margin line 344
16. def OAI.SharpNodal.Profiles.ScaledWave.rebase line 355
17. lemma OAI.SharpNodal.Profiles.ScaledWave.rebase_growth line 403
18. def OAI.SharpNodal.Profiles.UnitWave.scaled line 416
19. lemma OAI.SharpNodal.Profiles.frequency_at_earlier_scale line 429
20. lemma OAI.SharpNodal.Profiles.frequency_rebase_bottom line 443
21. theorem OAI.SharpNodal.Profiles.sequence_persistent_paths line 447
22. lemma OAI.SharpNodal.Profiles.finite_constant_subsequence line 498
23. def OAI.SharpNodal.Profiles.PersistentSquare line 507
24. theorem OAI.SharpNodal.Profiles.uniform_persistence_alternative line 517