OAI/Geometry/PolarProducts/StripMaps.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolarStrips.domain line 44
  2. def OAI.PolarStrips.tuple line 46
  3. theorem OAI.PolarStrips.tuple_apply line 50
  4. theorem OAI.PolarStrips.norm_tuple_sq line 53
  5. theorem OAI.PolarStrips.isOpen_domain line 61
  6. theorem OAI.PolarStrips.zero_mem_domain line 67
  7. theorem OAI.PolarStrips.analyticOnNhd_tuple line 71
  8. theorem OAI.PolarStrips.tuple_zero_iff line 78
  9. theorem OAI.PolarStrips.tuple_order line 93
  10. theorem OAI.PolarStrips.isBounded_domain line 109
  11. theorem OAI.PolarStrips.compact_inner_preimage line 125
  12. theorem OAI.PolarStrips.compact_sublevel line 137
  13. abbrev OAI.ComplexCoordinates.R line 190
  14. abbrev OAI.ComplexCoordinates.C line 191
  15. def OAI.ComplexCoordinates.re line 193
  16. def OAI.ComplexCoordinates.im line 199
  17. theorem OAI.ComplexCoordinates.re_apply line 205
  18. theorem OAI.ComplexCoordinates.im_apply line 206
  19. def OAI.ComplexCoordinates.parts line 208
  20. theorem OAI.ComplexCoordinates.parts_apply line 217
  21. theorem OAI.ComplexCoordinates.parts_symm_apply line 218
  22. def OAI.ComplexCoordinates.functional line 221
  23. theorem OAI.ComplexCoordinates.functional_apply line 227
  24. theorem OAI.ComplexCoordinates.re_functional line 229
  25. theorem OAI.ComplexCoordinates.im_functional line 233
  26. theorem OAI.ComplexCoordinates.norm_sq_parts line 237
  27. theorem OAI.ComplexCoordinates.real_inner_parts line 241
  28. theorem OAI.ComplexCoordinates.re_I_smul line 248
  29. theorem OAI.ComplexCoordinates.im_I_smul line 250
  30. theorem OAI.ComplexCoordinates.functional_injective line 253
  31. def OAI.PlanarLens.primitive line 276
  32. theorem OAI.PlanarLens.contDiffAt_primitive line 278
  33. theorem OAI.PlanarLens.J_mono line 282
  34. theorem OAI.PlanarLens.J_product_nonneg line 292
  35. theorem OAI.PlanarLens.fderiv_primitive_one line 299
  36. theorem OAI.PlanarLens.fderiv_primitive_apply line 312