OAI/Analysis/PlanarEndpoint/MaximalBridge.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.LocalMaximalBound line 16
  2. lemma OAI.PlanarEndpoint.integrableOn_evolutionPath_ball line 20
  3. lemma OAI.PlanarEndpoint.hThirdNorm_approx_le line 25
  4. lemma OAI.PlanarEndpoint.ae_summable_paths_of_unit_ball line 30
  5. lemma OAI.PlanarEndpoint.paths_tsum_finite_of_maximal line 44
  6. lemma OAI.PlanarEndpoint.pathLimit_integrable_of_uniform_bounds line 65
  7. lemma OAI.PlanarEndpoint.mainConclusion_of_localMaximalBound line 92