OAI/Analysis/PlanarEndpoint/GraphSelection.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. lemma OAI.PlanarEndpoint.graph_evolution_pairing_bound line 20
  2. def OAI.PlanarEndpoint.normingPhase line 42
  3. lemma OAI.PlanarEndpoint.normingPhase_measurable line 44
  4. lemma OAI.PlanarEndpoint.normingPhase_norm line 47
  5. lemma OAI.PlanarEndpoint.normingPhase_mul line 52
  6. lemma OAI.PlanarEndpoint.measurable_graph_evolution line 59
  7. lemma OAI.PlanarEndpoint.graph_evolution_norm_integrable line 65
  8. lemma OAI.PlanarEndpoint.graph_evolution_norm_bound line 76
  9. abbrev OAI.PlanarEndpoint.HalfTime line 95
  10. instance OAI.PlanarEndpoint.halfTime_nonempty line 96
  11. def OAI.PlanarEndpoint.denseTime line 98
  12. lemma OAI.PlanarEndpoint.denseTime_dense line 99
  13. lemma OAI.PlanarEndpoint.denseTime_bound line 101
  14. lemma OAI.PlanarEndpoint.exists_denseTime_near_path line 111
  15. lemma OAI.PlanarEndpoint.exists_measurable_near_time line 122
  16. lemma OAI.PlanarEndpoint.localMaximalBound_of_shortTime line 139
  17. lemma OAI.PlanarEndpoint.mainConclusion_of_shortTime line 161