OAI/Analysis/PlanarEndpoint/WeightedGraph.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. lemma OAI.PlanarEndpoint.annularCutoff_scaled_memLp line 19
  2. def OAI.PlanarEndpoint.normalizedGraphDensity line 24
  3. lemma OAI.PlanarEndpoint.normalizedGraphDensity_memLp line 29
  4. lemma OAI.PlanarEndpoint.integral_sq_norm_toLp line 36
  5. lemma OAI.PlanarEndpoint.normalizedGraphDensity_energy line 43
  6. lemma OAI.PlanarEndpoint.sobolevWeight_inv_le_dyadic line 57
  7. lemma OAI.PlanarEndpoint.unit_ball_real line 69
  8. lemma OAI.PlanarEndpoint.graphFourier_unit_bound line 72
  9. def OAI.PlanarEndpoint.graphLowMajorant line 79
  10. lemma OAI.PlanarEndpoint.graphLowMajorant_nonneg line 82
  11. lemma OAI.PlanarEndpoint.graphLowMajorant_integrable line 85
  12. lemma OAI.PlanarEndpoint.graphLowMajorant_integral line 89
  13. lemma OAI.PlanarEndpoint.graph_weighted_pointwise line 96
  14. lemma OAI.PlanarEndpoint.graph_weighted_integrableOn line 130
  15. lemma OAI.PlanarEndpoint.graph_weighted_sum_bound line 142