OAI/Geometry/PolarProducts/RadialMap.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialSymplectic.radialMap line 41
  2. def OAI.RadialSymplectic.radialPrimitive line 43
  3. theorem OAI.RadialSymplectic.fderiv_radialMap line 46
  4. theorem OAI.RadialSymplectic.fderiv_radialPrimitive line 54
  5. theorem OAI.RadialSymplectic.radial_pullback line 67
  6. def OAI.RadialSymplectic.radiusSq line 87
  7. def OAI.RadialSymplectic.inverseScaleSq line 89
  8. theorem OAI.RadialSymplectic.radiusSq_strictMonoOn line 92
  9. theorem OAI.RadialSymplectic.radial_discriminant_pos line 104
  10. theorem OAI.RadialSymplectic.inverseScaleSq_den_pos line 108
  11. theorem OAI.RadialSymplectic.inverseScaleSq_pos line 119
  12. theorem OAI.RadialSymplectic.inverseScaleSq_quadratic line 123
  13. theorem OAI.RadialSymplectic.radiusSq_inverse line 133
  14. theorem OAI.RadialSymplectic.inverseScaleSq_factor line 143
  15. theorem OAI.RadialSymplectic.contDiffAt_inverseScaleSq line 152
  16. def OAI.RadialSymplectic.expansionScale line 172
  17. def OAI.RadialSymplectic.radialExpansion line 173
  18. def OAI.RadialSymplectic.contractionScale line 174
  19. def OAI.RadialSymplectic.radialContraction line 176
  20. theorem OAI.RadialSymplectic.expansionScale_pos line 179
  21. theorem OAI.RadialSymplectic.expansionScale_sq line 187
  22. theorem OAI.RadialSymplectic.norm_sq_radialExpansion line 194
  23. theorem OAI.RadialSymplectic.radialExpansion_injective line 201
  24. theorem OAI.RadialSymplectic.contractionScale_pos line 215
  25. theorem OAI.RadialSymplectic.norm_sq_radialContraction line 219
  26. theorem OAI.RadialSymplectic.expansionScale_mul_contractionScale line 224
  27. theorem OAI.RadialSymplectic.radialExpansion_radialContraction line 235
  28. theorem OAI.RadialSymplectic.radialContraction_radialExpansion line 240
  29. theorem OAI.RadialSymplectic.contDiff_expansionScale line 244
  30. theorem OAI.RadialSymplectic.contDiff_contractionScale line 253
  31. theorem OAI.RadialSymplectic.contDiff_radialExpansion line 263
  32. theorem OAI.RadialSymplectic.contDiff_radialContraction line 267
  33. def OAI.RadialSymplectic.radialHomeomorph line 271
  34. theorem OAI.RadialSymplectic.radialContraction_mapsTo line 279
  35. def OAI.RadialSymplectic.modelPotential line 303
  36. theorem OAI.RadialSymplectic.contDiff_modelPotential line 305
  37. theorem OAI.RadialSymplectic.dc_modelPotential line 311
  38. theorem OAI.RadialSymplectic.radialExpansion_pullback line 328
  39. theorem OAI.RadialSymplectic.radialContraction_pullback line 342