OAI/MeasureTheory/FalconerCompletion/Graphs/DiagonalBinMassLe.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.diagonal_bin_mass_le line 19
  2. def OAI.GraphLiteralSupport.Attempt4FarGrid.realBin line 41
  3. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.realBin_measurable line 44
  4. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.realBin_disjoint line 47
  5. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.realBin_diameter line 60
  6. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.real_bin_collision_bound line 66
  7. def OAI.GraphLiteralSupport.Attempt4FarGrid.binL2Norm line 87
  8. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.ennreal_offset_cauchy line 90
  9. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.realBin_cover line 103
  10. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.offset_rectangles_mass_le line 110
  11. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.finite_offset_rectangles_mass_le line 118
  12. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.half_le_abs_int_add_half line 143
  13. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.realBin_kernel_bound line 152
  14. def OAI.GraphLiteralSupport.Attempt4FarGrid.binKernelWeight line 175
  15. def OAI.GraphLiteralSupport.Attempt4FarGrid.binKernelConstant line 178
  16. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.binKernelConstant_ne_top line 180
  17. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.weighted_offset_kernel_bound line 186
  18. theorem OAI.GraphLiteralSupport.Attempt4FarGrid.real_bin_decaying_kernel_bound line 206
  19. lemma OAI.GraphLiteralSupport.Attempt4FullFar.mixed_bin_collisionND line 247
  20. def OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistanceLawND line 267
  21. def OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistanceCountND line 270
  22. instance OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistanceLawND_finite line 274
  23. lemma OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistanceLawND_prod line 279
  24. lemma OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistanceLawND_collision line 285
  25. lemma OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistanceCountND_ne_top line 292
  26. lemma OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistanceCountND_unnormalized line 296
  27. theorem OAI.GraphLiteralSupport.Attempt4FullFar.positiveDistance_kernel_maxND line 306