OAI/Analysis/CoulombRadii/FieldAnalysis/GridIndex.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.cubeMass_nonneg line 118
  2. lemma OAI.Coulomb.grid_leading_summable line 121
  3. lemma OAI.Coulomb.grid_kinetic_lower line 129
  4. def OAI.Coulomb.gridIndex line 149
  5. lemma OAI.Coulomb.gridIndex_of_mem line 151
  6. lemma OAI.Coulomb.mem_gridBox_index line 166
  7. lemma OAI.Coulomb.gridIndex_measurable line 181
  8. lemma OAI.Coulomb.gridBox_hasSum_weighted line 191
  9. lemma OAI.Coulomb.grid_leading_expectation line 210
  10. lemma OAI.Coulomb.grid_count_expectation_kinetic_lower line 231
  11. lemma OAI.Coulomb.gridBox_volume line 241
  12. lemma OAI.Coulomb.sum_indicator_rpow_disjoint line 247
  13. def OAI.Coulomb.gridCellDensity line 265
  14. lemma OAI.Coulomb.cell_power_scaling line 271
  15. lemma OAI.Coulomb.gridCellDensity_power_integral line 279
  16. def OAI.Coulomb.sameCell1 line 317
  17. lemma OAI.Coulomb.sameCell1_nonneg line 319
  18. lemma OAI.Coulomb.sameCell1_le_one line 323
  19. lemma OAI.Coulomb.sameCell1_periodic line 327
  20. lemma OAI.Coulomb.sameCell1_measurable line 334
  21. lemma OAI.Coulomb.sameCell1_Ioc line 342
  22. lemma OAI.Coulomb.sameCell1_integral_zero line 353
  23. lemma OAI.Coulomb.sameCell1_integral line 377
  24. def OAI.Coulomb.sameGridCell line 395
  25. def OAI.Coulomb.flatFineKernel line 398
  26. lemma OAI.Coulomb.sameGridCell_integral line 401
  27. lemma OAI.Coulomb.sameGridCell_nonneg line 410
  28. lemma OAI.Coulomb.sameGridCell_le_one line 413
  29. lemma OAI.Coulomb.sameGridCell_measurable line 418
  30. lemma OAI.Coulomb.sameGridCell_integrable line 425
  31. def OAI.Coulomb.translatedGridDensity line 435
  32. lemma OAI.Coulomb.translatedGridDensity_integral line 439
  33. lemma OAI.Coulomb.sameCell1_eq_ite line 449
  34. lemma OAI.Coulomb.sameGridCell_eq_ite line 453
  35. lemma OAI.Coulomb.sum_fiber_weight line 468
  36. lemma OAI.Coulomb.gridCellDensity_sum_particles line 482
  37. lemma OAI.Coulomb.mem_gridBox_iff_index line 502
  38. lemma OAI.Coulomb.sameGridCell_eq_indicator line 510
  39. lemma OAI.Coulomb.translatedGridDensity_eq_cell line 515
  40. lemma OAI.Coulomb.translatedGridDensity_power_integral line 526