OAI/MeasureTheory/FalconerCompletion/Graphs/GraphJetMul.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.CurrentFalconer.graphJetMul line 19
  2. lemma OAI.CurrentFalconer.graphJetConj line 46
  3. lemma OAI.CurrentFalconer.graphJetPair line 54
  4. lemma OAI.CurrentFalconer.graphJet_enlarge line 67
  5. lemma OAI.CurrentFalconer.graphCapJet line 74
  6. lemma OAI.CurrentFalconer.graph_four_moment_bridge line 100
  7. lemma OAI.CurrentFalconer.graph_angular_four_integrable line 149
  8. def OAI.CurrentFalconer.graphCellLaw line 209
  9. instance OAI.CurrentFalconer.graphCellLaw_finite line 212
  10. lemma OAI.CurrentFalconer.graphCellLaw_ae line 219
  11. lemma OAI.CurrentFalconer.graphCellLaw_transform line 226
  12. lemma OAI.CurrentFalconer.graphCellLaw_mass line 235
  13. lemma OAI.CurrentFalconer.graph_four_integrable line 241
  14. theorem OAI.CurrentFalconer.graph_source_raw_four_decay line 293