OAI/Analysis/PlanarEndpoint/TimeTree.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. theorem OAI.PlanarEndpoint.TimeTree.convexity_deficit line 12
  2. structure OAI.PlanarEndpoint.TimeTree.MassTree line 39
  3. def OAI.PlanarEndpoint.TimeTree.MassTree.lighterMass line 47
  4. def OAI.PlanarEndpoint.TimeTree.MassTree.deficit line 49
  5. lemma OAI.PlanarEndpoint.TimeTree.MassTree.lighterMass_nonneg line 52
  6. lemma OAI.PlanarEndpoint.TimeTree.MassTree.deficit_nonneg line 55
  7. lemma OAI.PlanarEndpoint.TimeTree.MassTree.lighterMass_bound line 61
  8. def OAI.PlanarEndpoint.TimeTree.level line 75
  9. lemma OAI.PlanarEndpoint.TimeTree.mem_level line 79
  10. lemma OAI.PlanarEndpoint.TimeTree.level_children_disjoint line 88
  11. lemma OAI.PlanarEndpoint.TimeTree.sum_level_succ line 96
  12. def OAI.PlanarEndpoint.TimeTree.internal line 102
  13. lemma OAI.PlanarEndpoint.TimeTree.mem_internal line 105
  14. lemma OAI.PlanarEndpoint.TimeTree.internal_succ line 109
  15. lemma OAI.PlanarEndpoint.TimeTree.internal_level_disjoint line 114
  16. lemma OAI.PlanarEndpoint.TimeTree.sum_internal line 120
  17. def OAI.PlanarEndpoint.TimeTree.MassTree.potential line 131
  18. lemma OAI.PlanarEndpoint.TimeTree.MassTree.potential_nonneg line 133
  19. lemma OAI.PlanarEndpoint.TimeTree.MassTree.sum_deficit_level line 136
  20. lemma OAI.PlanarEndpoint.TimeTree.MassTree.deficits_telescope line 143
  21. lemma OAI.PlanarEndpoint.TimeTree.MassTree.sum_deficit_internal line 152
  22. lemma OAI.PlanarEndpoint.TimeTree.MassTree.potential_le_root line 161
  23. lemma OAI.PlanarEndpoint.TimeTree.MassTree.deficit_sum_le_root line 168
  24. lemma OAI.PlanarEndpoint.TimeTree.MassTree.convexity_constant_pos line 181
  25. lemma OAI.PlanarEndpoint.TimeTree.MassTree.lighterMass_sum_le line 185
  26. lemma OAI.PlanarEndpoint.TimeTree.MassTree.lighterMass_summable line 192
  27. lemma OAI.PlanarEndpoint.TimeTree.MassTree.lighterMass_tsum_le line 197
  28. def OAI.PlanarEndpoint.TimeTree.MassTree.heavy line 202
  29. def OAI.PlanarEndpoint.TimeTree.MassTree.light line 205
  30. lemma OAI.PlanarEndpoint.TimeTree.MassTree.light_mass line 208
  31. lemma OAI.PlanarEndpoint.TimeTree.MassTree.heavy_injective line 214
  32. def OAI.PlanarEndpoint.TimeTree.MassTree.heavyPath line 219
  33. lemma OAI.PlanarEndpoint.TimeTree.MassTree.heavyPath_injective line 221
  34. lemma OAI.PlanarEndpoint.TimeTree.MassTree.heavyPath_length line 224
  35. lemma OAI.PlanarEndpoint.TimeTree.MassTree.offspring_sum_le line 233
  36. def OAI.PlanarEndpoint.TimeTree.MassTree.offspringPenalty line 240
  37. lemma OAI.PlanarEndpoint.TimeTree.MassTree.offspringPenalty_nonneg line 243
  38. lemma OAI.PlanarEndpoint.TimeTree.MassTree.offspringPenalty_sum_le line 247
  39. lemma OAI.PlanarEndpoint.TimeTree.MassTree.terminal_sum_le line 269
  40. def OAI.PlanarEndpoint.TimeTree.MassTree.pathBudget line 287
  41. lemma OAI.PlanarEndpoint.TimeTree.MassTree.pathBudget_nonneg line 290
  42. lemma OAI.PlanarEndpoint.TimeTree.MassTree.geom_sum_le line 295
  43. lemma OAI.PlanarEndpoint.TimeTree.MassTree.next_geom_sum_le line 301
  44. lemma OAI.PlanarEndpoint.TimeTree.MassTree.pathBudget_internal_le line 307
  45. lemma OAI.PlanarEndpoint.TimeTree.MassTree.pathBudget_sum_le line 328
  46. lemma OAI.PlanarEndpoint.TimeTree.MassTree.pathBudget_summable line 339
  47. lemma OAI.PlanarEndpoint.TimeTree.MassTree.pathBudget_tsum_le line 343
  48. lemma OAI.PlanarEndpoint.TimeTree.MassTree.heavy_light_mass line 348
  49. lemma OAI.PlanarEndpoint.TimeTree.MassTree.heavy_mass_le line 353
  50. lemma OAI.PlanarEndpoint.TimeTree.MassTree.heavyPath_mass_le line 357
  51. lemma OAI.PlanarEndpoint.TimeTree.MassTree.light_length line 365
  52. lemma OAI.PlanarEndpoint.TimeTree.MassTree.heavy_light_add line 369
  53. lemma OAI.PlanarEndpoint.TimeTree.MassTree.heavyPath_partition line 375
  54. lemma OAI.PlanarEndpoint.TimeTree.MassTree.norm_heavyPath_le line 388
  55. lemma OAI.PlanarEndpoint.TimeTree.weighted_norm_sum_sq line 399
  56. def OAI.PlanarEndpoint.TimeTree.MassTree.pathPiece line 414
  57. lemma OAI.PlanarEndpoint.TimeTree.MassTree.sum_pathPiece line 417
  58. def OAI.PlanarEndpoint.TimeTree.MassTree.pathWeight line 427
  59. lemma OAI.PlanarEndpoint.TimeTree.MassTree.pathWeight_nonneg line 430
  60. lemma OAI.PlanarEndpoint.TimeTree.MassTree.sum_pathWeight_le line 435
  61. lemma OAI.PlanarEndpoint.TimeTree.MassTree.energy_le_pathBudget line 453
  62. lemma OAI.PlanarEndpoint.TimeTree.MassTree.common_tree_energy_sum_le line 505
  63. lemma OAI.PlanarEndpoint.TimeTree.MassTree.common_tree_energy_tsum_le line 537