OAI/Analysis/NodalLength/ScaledWaves.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Profiles.rescaleMap line 189
  2. lemma OAI.SharpNodal.Profiles.smooth_rescaleMap line 191
  3. lemma OAI.SharpNodal.Profiles.partial_rescale line 195
  4. lemma OAI.SharpNodal.Profiles.laplacian_rescale line 208
  5. lemma OAI.SharpNodal.Profiles.partial_rescale_local line 221
  6. lemma OAI.SharpNodal.Profiles.laplacian_rescale_local line 232
  7. lemma OAI.SharpNodal.Profiles.rescaleMap_ball_preimage line 242
  8. lemma OAI.SharpNodal.Profiles.map_volume_rescaleMap line 250
  9. lemma OAI.SharpNodal.Profiles.centeredMass_rescale line 260
  10. lemma OAI.SharpNodal.Profiles.centered_excess_rescale line 295
  11. structure OAI.SharpNodal.Profiles.ScaledWave line 312
  12. lemma OAI.SharpNodal.Profiles.rescaleMap_mapsTo line 319
  13. lemma OAI.SharpNodal.Profiles.grid_expect line 329
  14. def OAI.SharpNodal.Profiles.ScaledWave.child line 337
  15. lemma OAI.SharpNodal.Profiles.ScaledWave.child_growth line 421
  16. def OAI.SharpNodal.Profiles.GridChild line 436
  17. def OAI.SharpNodal.Profiles.DescentRule line 441
  18. theorem OAI.SharpNodal.Profiles.actual_descent_rule line 449
  19. def OAI.SharpNodal.Descent.Tree.ScaledFloors line 487
  20. lemma OAI.SharpNodal.Descent.Tree.scaled_floor_bound line 492
  21. lemma OAI.SharpNodal.Descent.Tree.physical_floor_bound line 526
  22. inductive OAI.SharpNodal.Profiles.WaveTree line 548
  23. def OAI.SharpNodal.Profiles.WaveTree.rootWave line 555
  24. def OAI.SharpNodal.Profiles.WaveTree.rootTilt line 559
  25. def OAI.SharpNodal.Profiles.WaveTree.label line 563
  26. def OAI.SharpNodal.Profiles.WaveTree.numerical line 566
  27. lemma OAI.SharpNodal.Profiles.WaveTree.numerical_root line 570
  28. def OAI.SharpNodal.Profiles.WaveTree.Coherent line 573
  29. def OAI.SharpNodal.Profiles.WaveTree.Stopped line 578
  30. lemma OAI.SharpNodal.Profiles.WaveTree.coherent_floors line 584
  31. lemma OAI.SharpNodal.Profiles.WaveTree.label_nonnegative line 598
  32. theorem OAI.SharpNodal.Profiles.WaveTree.build_stopped line 604
  33. lemma OAI.SharpNodal.Profiles.stable_band_large_slope line 645
  34. theorem OAI.SharpNodal.Profiles.actual_tree_stability line 664