OAI/Analysis/CoulombIonization/FieldAnalysis/CubeRotations.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CoulombNeumann.CubeSpace line 16
  2. abbrev OAI.CoulombNeumann.CubeRotation line 18
  3. instance OAI.CoulombNeumann.cubeSpace_continuousStar line 20
  4. instance OAI.CoulombNeumann.cubeRotation_compact line 23
  5. def OAI.CoulombNeumann.cubeRotationMeasure line 30
  6. instance OAI.CoulombNeumann.cubeRotation_probability line 33
  7. instance OAI.CoulombNeumann.cubeRotation_leftInvariant line 36
  8. def OAI.CoulombNeumann.rotationIsometry line 40
  9. lemma OAI.CoulombNeumann.rotationIsometry_apply line 43
  10. lemma OAI.CoulombNeumann.rotationIsometry_continuous line 46
  11. lemma OAI.CoulombNeumann.rotationIsometry_inv_mul line 49
  12. def OAI.CoulombNeumann.radialAverage line 60
  13. lemma OAI.CoulombNeumann.radialAverage_joint_measurable line 63
  14. lemma OAI.CoulombNeumann.radialAverage_measurable line 68
  15. lemma OAI.CoulombNeumann.radialAverage_section_integrable line 72
  16. lemma OAI.CoulombNeumann.radialAverage_nonneg line 79
  17. lemma OAI.CoulombNeumann.radialAverage_le line 82
  18. lemma OAI.CoulombNeumann.radialAverage_rotation line 90
  19. lemma OAI.CoulombNeumann.radialAverage_radial line 96
  20. lemma OAI.CoulombNeumann.radialAverage_support line 105
  21. lemma OAI.CoulombNeumann.radialAverage_joint_integrable line 113
  22. lemma OAI.CoulombNeumann.radialAverage_integrable line 125
  23. lemma OAI.CoulombNeumann.integral_radialAverage line 128