OAI/Analysis/PlanarEndpoint/DyadicGraph.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. def OAI.PlanarEndpoint.DyadicGraph.width line 14
  2. def OAI.PlanarEndpoint.DyadicGraph.left line 16
  3. def OAI.PlanarEndpoint.DyadicGraph.interval line 21
  4. lemma OAI.PlanarEndpoint.DyadicGraph.width_pos line 23
  5. lemma OAI.PlanarEndpoint.DyadicGraph.width_cons line 25
  6. lemma OAI.PlanarEndpoint.DyadicGraph.interval_nil line 29
  7. lemma OAI.PlanarEndpoint.DyadicGraph.interval_false line 31
  8. lemma OAI.PlanarEndpoint.DyadicGraph.interval_true line 35
  9. lemma OAI.PlanarEndpoint.DyadicGraph.interval_split line 41
  10. lemma OAI.PlanarEndpoint.DyadicGraph.interval_disjoint line 46
  11. lemma OAI.PlanarEndpoint.DyadicGraph.interval_child_subset line 53
  12. lemma OAI.PlanarEndpoint.DyadicGraph.interval_subset_root line 60
  13. lemma OAI.PlanarEndpoint.DyadicGraph.interval_measurable line 65
  14. lemma OAI.PlanarEndpoint.DyadicGraph.interval_level_partition line 67
  15. def OAI.PlanarEndpoint.DyadicGraph.index line 86
  16. lemma OAI.PlanarEndpoint.DyadicGraph.index_lt line 91
  17. lemma OAI.PlanarEndpoint.DyadicGraph.index_injective line 96
  18. lemma OAI.PlanarEndpoint.DyadicGraph.left_eq line 111
  19. lemma OAI.PlanarEndpoint.DyadicGraph.interval_eq line 118
  20. lemma OAI.PlanarEndpoint.DyadicGraph.sum_level line 124
  21. def OAI.PlanarEndpoint.DyadicGraph.fiber line 138
  22. lemma OAI.PlanarEndpoint.DyadicGraph.fiber_split line 140
  23. lemma OAI.PlanarEndpoint.DyadicGraph.fiber_disjoint line 144
  24. lemma OAI.PlanarEndpoint.DyadicGraph.fiber_measurable line 148
  25. def OAI.PlanarEndpoint.DyadicGraph.massTree line 152
  26. lemma OAI.PlanarEndpoint.DyadicGraph.massTree_root line 159
  27. lemma OAI.PlanarEndpoint.DyadicGraph.restrict_fiber_split line 169
  28. def OAI.PlanarEndpoint.DyadicGraph.vector line 175
  29. lemma OAI.PlanarEndpoint.DyadicGraph.vector_split line 181
  30. lemma OAI.PlanarEndpoint.DyadicGraph.vector_level_sum line 192
  31. lemma OAI.PlanarEndpoint.DyadicGraph.mass_level_sum line 200