OAI/Analysis/CoulombRadii/FieldAnalysis/PhaseRegion.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.volume_real_ball_three line 83
  2. lemma OAI.Coulomb.integral_ball_norm_sq_three line 89
  3. lemma OAI.Coulomb.integrableOn_ball_norm_sq_three line 111
  4. def OAI.Coulomb.phaseRegion line 116
  5. def OAI.Coulomb.phaseMeasure line 118
  6. lemma OAI.Coulomb.phaseRegion_measurable line 120
  7. lemma OAI.Coulomb.phaseMeasure_le line 123
  8. lemma OAI.Coulomb.phaseMeasure_lintegral line 126
  9. lemma OAI.Coulomb.phaseMeasure_mass line 138
  10. lemma OAI.Coulomb.phaseMeasure_lintegral_momentum line 144
  11. lemma OAI.Coulomb.phaseMeasure_momentum_memLp line 154
  12. lemma OAI.Coulomb.phaseMeasure_real_momentum line 165
  13. def OAI.Coulomb.fermiRadius line 173
  14. lemma OAI.Coulomb.fermiRadius_nonneg line 175
  15. lemma OAI.Coulomb.fermiRadius_cube line 177
  16. lemma OAI.Coulomb.fermiRadius_fifth line 181
  17. lemma OAI.Coulomb.fermiRadius_measurable line 185
  18. lemma OAI.Coulomb.fermiRadius_ball_mass line 189
  19. lemma OAI.Coulomb.fermiMeasure_mass line 197
  20. lemma OAI.Coulomb.fermiMeasure_finite line 205
  21. lemma OAI.Coulomb.fermiMeasure_momentum_memLp line 211