OAI/Analysis/PlanarEndpoint/GraphDistribution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. def OAI.PlanarEndpoint.SourceGraphDistribution line 15
  2. lemma OAI.PlanarEndpoint.graphDistribution_scale_identity line 24
  3. lemma OAI.PlanarEndpoint.unitFrequencyGraphEstimate_of_source line 39
  4. lemma OAI.PlanarEndpoint.sourceGraphDistribution_of_unitFrequency line 53
  5. lemma OAI.PlanarEndpoint.mainConclusion_of_sourceGraphDistribution line 65