OAI/MeasureTheory/FalconerCompletion/Graphs/IntervalRamp.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.intervalRamp line 15
  2. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.intervalRamp_increment line 17
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.finiteRampProfile line 24
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.finiteRampProfile_continuous line 27
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.intervalRamp_sum line 34
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.finiteRampProfile_zero line 40
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.finiteRampProfile_increment line 44
  8. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockSlope line 68
  9. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizedProfile line 73
  10. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockSlope_bounds line 77
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizedProfile_continuous line 103
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizedProfile_zero line 107
  13. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizedProfile_increment line 111
  14. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizedProfile_adjusted_increment line 123
  15. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.intervalRamp_at_upper line 132
  16. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.intervalRamp_at_lower line 135
  17. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.intervalRamp_of_le line 138
  18. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.intervalRamp_of_ge line 141
  19. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.finiteRampProfile_block_difference line 144
  20. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.finiteRampProfile_knots_telescope line 163
  21. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockSlope_mul_gap line 174
  22. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockLogProduct line 188
  23. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.blockProduct_eq_pow line 193
  24. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizedProfile_grid line 198
  25. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizedProfile_reference_grid line 222
  26. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.finiteRampProfile_affine_block line 236
  27. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.massBinCandidates line 266
  28. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafMassBin line 270
  29. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.massBinCandidates_nonempty line 273
  30. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafMassBin_le line 278
  31. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafMassBin_lower line 286
  32. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafMassBin_upper line 293
  33. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafBinEndpoint line 309
  34. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafBinEndpoint_pos line 311
  35. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leaf_mass_bin_bounds line 314
  36. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.ratio_bounds_of_mass_bounds line 327