OAI/Analysis/CoulombIonization/FieldAnalysis/Vartheta.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombNeumann.euclideanCubeOverlap line 17
  2. lemma OAI.CoulombNeumann.euclideanCubeOverlap_measurable line 19
  3. lemma OAI.CoulombNeumann.euclideanCubeOverlap_integrable line 22
  4. lemma OAI.CoulombNeumann.integral_euclideanCubeOverlap line 25
  5. lemma OAI.CoulombNeumann.euclideanCubeOverlap_support line 30
  6. def OAI.CoulombNeumann.vartheta line 45
  7. lemma OAI.CoulombNeumann.vartheta_measurable line 47
  8. lemma OAI.CoulombNeumann.vartheta_integrable line 48
  9. lemma OAI.CoulombNeumann.vartheta_nonneg line 49
  10. lemma OAI.CoulombNeumann.vartheta_le line 50
  11. lemma OAI.CoulombNeumann.integral_vartheta line 52
  12. lemma OAI.CoulombNeumann.vartheta_radial line 55
  13. lemma OAI.CoulombNeumann.vartheta_support line 56
  14. def OAI.CoulombNeumann.varthetaScaled line 59
  15. lemma OAI.CoulombNeumann.varthetaScaled_measurable line 61
  16. lemma OAI.CoulombNeumann.varthetaScaled_integrable line 63
  17. lemma OAI.CoulombNeumann.varthetaScaled_nonneg line 65
  18. lemma OAI.CoulombNeumann.varthetaScaled_le line 67
  19. lemma OAI.CoulombNeumann.integral_varthetaScaled line 69
  20. lemma OAI.CoulombNeumann.varthetaScaled_radial line 73
  21. lemma OAI.CoulombNeumann.varthetaScaled_support line 77
  22. lemma OAI.CoulombNeumann.cubeDensity_measurable line 89
  23. lemma OAI.CoulombNeumann.cubeAssignment_measurable line 98
  24. lemma OAI.CoulombNeumann.cubePressure_measurable line 104
  25. lemma OAI.CoulombNeumann.cube_t_continuous line 108
  26. lemma OAI.CoulombNeumann.translation_average_pressure line 111
  27. def OAI.CoulombNeumann.varthetaSmear line 129
  28. def OAI.CoulombNeumann.rotatedCubeCloud line 132
  29. def OAI.CoulombNeumann.translatedPressureAverage line 135
  30. lemma OAI.CoulombNeumann.translatedPressureAverage_measurable line 138
  31. lemma OAI.CoulombNeumann.translatedPressureAverage_nonneg line 142
  32. lemma OAI.CoulombNeumann.translatedPressureAverage_le line 144
  33. lemma OAI.CoulombNeumann.rotatedCubeCloud_continuous line 151
  34. lemma OAI.CoulombNeumann.varthetaSmear_translation_rotation line 159
  35. lemma OAI.CoulombNeumann.cubeOverlap_sum_integrable line 173
  36. lemma OAI.CoulombNeumann.cubeOverlap_sum_le line 177
  37. lemma OAI.CoulombNeumann.rotatedCloud_coordinates_preserving line 183
  38. lemma OAI.CoulombNeumann.rotatedCloud_coordinates_embedding line 187
  39. lemma OAI.CoulombNeumann.rotatedCloud_density_measurable line 192
  40. def OAI.CoulombNeumann.radialPressureAverage line 203
  41. lemma OAI.CoulombNeumann.radialPressureAverage_measurable line 206
  42. lemma OAI.CoulombNeumann.radialPressureAverage_nonneg line 209
  43. lemma OAI.CoulombNeumann.translatedPressureAverage_rotation_integrable line 212
  44. lemma OAI.CoulombNeumann.radialPressureAverage_le line 222
  45. theorem OAI.CoulombNeumann.varthetaSmear_pressure line 226