OAI/MeasureTheory/FalconerCompletion/Graphs/ScalarPairSymbol.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.scalarPairSymbolND line 26
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.scalarPairSymbolND_measurable line 28
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.physical_pairAxis_measurable line 34
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.physical_kernel_joint_integrableND line 45
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.physical_energy_identityND line 91
  6. def OAI.GraphLiteralSupport.CurrentFalconer.physicalCrossMomentND line 177
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.physical_pair_crossND line 184
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.physicalCrossMomentND_swap line 203
  9. theorem OAI.GraphLiteralSupport.CurrentFalconer.physical_cross_energy_identityND line 210
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPairSourceSymbol_eq_scalarPair line 286
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actual_transform_uniform_package line 294
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actual_energy_identityND line 336