OAI/Analysis/NodalLength/Excursions.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Profiles.fieldGrowth line 221
  2. lemma OAI.SharpNodal.Profiles.UnitWave.growth_zero line 224
  3. def OAI.SharpNodal.Profiles.pathGrowth line 227
  4. def OAI.SharpNodal.Profiles.PathHigh line 232
  5. lemma OAI.SharpNodal.Profiles.HighWavePath.raw line 237
  6. def OAI.SharpNodal.Profiles.activeGrowth line 248
  7. def OAI.SharpNodal.Profiles.WaveTree.StopsAtLow line 254
  8. theorem OAI.SharpNodal.Profiles.WaveTree.build_untilted_stopped line 260
  9. lemma OAI.SharpNodal.Profiles.WaveTree.active_average_le_cost line 289
  10. def OAI.SharpNodal.Profiles.excursionCostConstant line 347
  11. lemma OAI.SharpNodal.Profiles.excursionCostConstant_nonneg line 350
  12. theorem OAI.SharpNodal.Profiles.active_terminal_average line 355
  13. def OAI.SharpNodal.Grid.atLevel line 388
  14. lemma OAI.SharpNodal.Grid.mem_atLevel line 390
  15. lemma OAI.SharpNodal.Grid.eq_atLevel line 395
  16. def OAI.SharpNodal.Grid.fullTree line 398
  17. lemma OAI.SharpNodal.Grid.mem_fullTree line 401
  18. lemma OAI.SharpNodal.Grid.atLevel_mem_fullTree line 417
  19. def OAI.SharpNodal.Grid.entries line 422
  20. lemma OAI.SharpNodal.Grid.entries_subset line 426
  21. lemma OAI.SharpNodal.Grid.entry_high line 429
  22. lemma OAI.SharpNodal.Grid.entry_separation line 432
  23. lemma OAI.SharpNodal.Grid.entry_parent_low line 439
  24. lemma OAI.SharpNodal.Grid.entries_on_high_suffix line 448
  25. lemma OAI.SharpNodal.Grid.smaller_entries_high_suffix line 465
  26. def OAI.SharpNodal.Grid.activeSet line 495
  27. lemma OAI.SharpNodal.Grid.terminal_has_active_entry line 498
  28. theorem OAI.SharpNodal.Grid.terminal_sum_le line 537
  29. theorem OAI.SharpNodal.Grid.terminal_mean_of_witnesses line 578