OAI/Analysis/PlanarEndpoint/UnitReduction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. def OAI.PlanarEndpoint.UnitFrequencyGraphEstimate line 20
  2. lemma OAI.PlanarEndpoint.inverse_smul_ball line 29
  3. lemma OAI.PlanarEndpoint.unitGraph_time_range line 38
  4. lemma OAI.PlanarEndpoint.unitGraph_threshold_identity line 50
  5. lemma OAI.PlanarEndpoint.shortTimeGraphEstimate_of_unitFrequency line 64
  6. lemma OAI.PlanarEndpoint.shortTimeWeakEstimate_of_unitFrequency line 119
  7. lemma OAI.PlanarEndpoint.mainConclusion_of_unitFrequencyGraph line 123