OAI/MeasureTheory/FalconerCompletion/Graphs/GraphPerp2.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.graphPerpND line 18
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.graphPerpND_sub line 20
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.graphPerpND_add line 24
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.graphPerpND_norm_le line 28
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.graphPerpND_change_direction line 35
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.graph_witness_tubeND line 49
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.graph_scalar_perp_ballND line 65
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.graph_phase_changeND line 77
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.graph_perp_center_changeND line 87
  10. def OAI.GraphLiteralSupport.CurrentFalconer.graphAffineLineND line 95
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.graphAffineLineND_nonempty line 97
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.graphPerpND_sub_smul line 100
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.infDist_graphAffineLineND line 105