OAI/Analysis/CoulombIonization/FieldAnalysis/CubeTiling.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombNeumann.floorCube line 18
  2. def OAI.CoulombNeumann.closedCube line 19
  3. def OAI.CoulombNeumann.cubeShift line 20
  4. lemma OAI.CoulombNeumann.floorCube_pi line 23
  5. lemma OAI.CoulombNeumann.floorCube_measurable line 28
  6. lemma OAI.CoulombNeumann.floorCube_disjoint line 33
  7. lemma OAI.CoulombNeumann.floorCube_cover line 42
  8. lemma OAI.CoulombNeumann.floorCube_restrict line 47
  9. lemma OAI.CoulombNeumann.cubeShift_preserving line 54
  10. lemma OAI.CoulombNeumann.integral_cubeShift line 72
  11. lemma OAI.CoulombNeumann.hasSum_integral_cubes line 80
  12. def OAI.CoulombNeumann.cubeChar line 95
  13. def OAI.CoulombNeumann.cubeOverlap line 97
  14. lemma OAI.CoulombNeumann.cubeChar_measurable line 99
  15. lemma OAI.CoulombNeumann.cubeChar_nonneg line 103
  16. lemma OAI.CoulombNeumann.cubeChar_le line 108
  17. lemma OAI.CoulombNeumann.volume_floorCube line 112
  18. lemma OAI.CoulombNeumann.cubeChar_integrable line 116
  19. lemma OAI.CoulombNeumann.integral_cubeChar line 119
  20. lemma OAI.CoulombNeumann.cubeOverlap_section_integrable line 124
  21. lemma OAI.CoulombNeumann.cubeOverlap_nonneg line 132
  22. lemma OAI.CoulombNeumann.cubeOverlap_le line 135
  23. lemma OAI.CoulombNeumann.cubeOverlap_measurable line 140
  24. lemma OAI.CoulombNeumann.cubeOverlap_convolution line 146
  25. lemma OAI.CoulombNeumann.cubeOverlap_integrable line 154
  26. lemma OAI.CoulombNeumann.integral_cubeOverlap line 159
  27. lemma OAI.CoulombNeumann.cubeChar_eq_zero_of_not_mem line 164
  28. lemma OAI.CoulombNeumann.cubeChar_pos_iff line 168
  29. lemma OAI.CoulombNeumann.cubeChar_coord line 173
  30. lemma OAI.CoulombNeumann.cubeOverlap_support_coord line 177
  31. lemma OAI.CoulombNeumann.lintegral_cube_periodization line 190