OAI/Analysis/NodalLength/TerminalGrid.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Grid.wordPoint line 226
  2. lemma OAI.SharpNodal.Grid.wordPoint_mem line 229
  3. lemma OAI.SharpNodal.Grid.wordPoint_injective line 239
  4. lemma OAI.SharpNodal.Grid.image_wordPoint line 248
  5. lemma OAI.SharpNodal.Grid.sum_wordPoint line 258
  6. lemma OAI.SharpNodal.Grid.wordPoint_zero line 262
  7. def OAI.SharpNodal.Grid.childPos line 266
  8. lemma OAI.SharpNodal.Grid.wordPoint_succ line 268
  9. def OAI.SharpNodal.Grid.cellScale line 275
  10. def OAI.SharpNodal.Grid.cellMap line 277
  11. def OAI.SharpNodal.Grid.gridGrowth line 280
  12. lemma OAI.SharpNodal.Grid.cellScale_succ line 283
  13. lemma OAI.SharpNodal.Grid.cellMap_child line 289
  14. lemma OAI.SharpNodal.Grid.pathGrowth_grid line 301
  15. lemma OAI.SharpNodal.Grid.pathHigh_grid line 314
  16. lemma OAI.SharpNodal.Grid.pathHigh_activeSet line 350
  17. lemma OAI.SharpNodal.Grid.activeGrowth_sum line 365
  18. theorem OAI.SharpNodal.Grid.active_grid_sum line 383
  19. def OAI.SharpNodal.Grid.Cell.parent line 409
  20. def OAI.SharpNodal.Grid.cellDigit line 411
  21. lemma OAI.SharpNodal.Grid.childPos_parent line 414
  22. lemma OAI.SharpNodal.Grid.cellMap_parent line 421
  23. lemma OAI.SharpNodal.Grid.cellScale_parent line 427
  24. lemma OAI.SharpNodal.Grid.Cell.subset_parent line 431
  25. lemma OAI.SharpNodal.Grid.Cell.parent_mem_fullTree line 438
  26. lemma OAI.SharpNodal.Grid.Cell.smallerAt_card_le line 445
  27. theorem OAI.SharpNodal.Grid.aligned_waves line 455
  28. def OAI.SharpNodal.Grid.offsetPos line 498
  29. lemma OAI.SharpNodal.Grid.cellScale_offset line 500
  30. lemma OAI.SharpNodal.Grid.cellMap_offset line 506
  31. lemma OAI.SharpNodal.Grid.offset_points_near line 518
  32. lemma OAI.SharpNodal.Grid.parent_near_in_child line 551
  33. lemma OAI.SharpNodal.Grid.Cell.parent_near line 565
  34. lemma OAI.SharpNodal.Grid.side_card_comparison line 571
  35. lemma OAI.SharpNodal.Grid.fieldGrowth_rescale line 578
  36. lemma OAI.SharpNodal.Grid.gridGrowth_child line 584
  37. def OAI.SharpNodal.Grid.goodWordPoints line 601
  38. lemma OAI.SharpNodal.Grid.goodWordPoints_subset line 604
  39. lemma OAI.SharpNodal.Grid.goodWordPoints_card line 610
  40. theorem OAI.SharpNodal.Grid.entry_witness line 626
  41. lemma OAI.SharpNodal.Grid.gridChild_growth line 709
  42. def OAI.SharpNodal.Grid.entryBound line 717
  43. lemma OAI.SharpNodal.Grid.entryBound_nonneg line 720
  44. lemma OAI.SharpNodal.Grid.entry_growth_grid line 724
  45. lemma OAI.SharpNodal.Grid.entry_level_lt line 744
  46. theorem OAI.SharpNodal.Grid.terminal_mean_grid line 756
  47. lemma OAI.SharpNodal.Grid.cellScale_root line 815
  48. lemma OAI.SharpNodal.Grid.cellMap_root line 820
  49. theorem OAI.SharpNodal.Grid.uniform_terminal_growth line 826