OAI/Analysis/CoulombRadii/FieldAnalysis/MeridianMap.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.meridianMap line 100
  2. def OAI.Coulomb.meridianDomain line 101
  3. lemma OAI.Coulomb.meridianDomain_measurable line 102
  4. lemma OAI.Coulomb.meridian_radicand_pos line 104
  5. def OAI.Coulomb.meridianDeriv line 108
  6. lemma OAI.Coulomb.meridian_hasFDeriv line 111
  7. lemma OAI.Coulomb.meridian_det line 122
  8. lemma OAI.Coulomb.meridianMap_injOn line 125
  9. lemma OAI.Coulomb.meridian_image line 137
  10. lemma OAI.Coulomb.meridian_lintegral line 153
  11. lemma OAI.Coulomb.plane_radial_lintegral line 169
  12. lemma OAI.Coulomb.axisymmetric_lintegral line 195
  13. lemma OAI.Coulomb.meridian_lintegral_iterated line 233
  14. def OAI.Coulomb.tripleSpaceEquiv line 253
  15. lemma OAI.Coulomb.tripleSpaceEquiv_apply line 257
  16. lemma OAI.Coulomb.tripleSpaceEquiv_preserving line 261
  17. lemma OAI.Coulomb.norm_tripleSpaceEquiv line 267
  18. lemma OAI.Coulomb.axisymmetric_space_lintegral line 271
  19. lemma OAI.Coulomb.angular_coulomb_integral line 285
  20. lemma OAI.Coulomb.affine_halfpower_intervalIntegrable line 303
  21. lemma OAI.Coulomb.meridian_coulomb_integral line 309
  22. lemma OAI.Coulomb.meridian_coulomb_lintegral line 323
  23. lemma OAI.Coulomb.norm_axis_sub_rpow line 335
  24. lemma OAI.Coulomb.radial_axis_coulomb_lintegral line 345
  25. lemma OAI.Coulomb.radial_space_lintegral line 371
  26. lemma OAI.Coulomb.radial_coulomb_lintegral line 391
  27. lemma OAI.Coulomb.radial_coulomb_lintegral_le line 409
  28. lemma OAI.Coulomb.radial_coulomb_lintegral_eq line 432
  29. lemma OAI.Coulomb.space_axis_continuous line 456
  30. lemma OAI.Coulomb.radial_coulomb_integral_le line 463
  31. lemma OAI.Coulomb.radial_coulomb_integral_eq line 483