OAI/MeasureTheory/FalconerCompletion/Graphs/GraphFixedSpatialTerm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.Attempt4FullFar.graphFixedSpatialTermND line 17
  2. lemma OAI.Attempt4FullFar.canonicalSphereMeasureND_prod_ae_norm line 21
  3. lemma OAI.Attempt4FullFar.spherePlaneWaveND_norm line 32
  4. lemma OAI.Attempt4FullFar.graphFixedSpatialTermND_radial line 36
  5. lemma OAI.Attempt4FullFar.graphFixedSpatialTermND_swap line 90
  6. lemma OAI.Attempt4FullFar.graph_center_scalar_error line 98
  7. lemma OAI.Attempt4FullFar.graphFixedSpatialTermND_angular_bound line 120
  8. lemma OAI.Attempt4FullFar.graphFixedSpatialTermND_radial_bound line 172
  9. theorem OAI.Attempt4FullFar.graph_fixed_nonedge_term_uniform line 253