OAI/Analysis/StrictMeans/HalfPlane.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.cayleyToHalfPlane line 25
  2. theorem OAI.StrictInverseFirstPower.one_sub_ne_zero_of_mem_disk line 27
  3. theorem OAI.StrictInverseFirstPower.cayley_im_mul_norm_sq line 33
  4. theorem OAI.StrictInverseFirstPower.cayley_mem_halfPlane line 42
  5. theorem OAI.StrictInverseFirstPower.cayley_differentiableOn line 52
  6. def OAI.StrictInverseFirstPower.cayleyToDisk line 59
  7. lemma OAI.StrictInverseFirstPower.add_I_ne_zero line 61
  8. lemma OAI.StrictInverseFirstPower.cayleyToDisk_mem line 67
  9. lemma OAI.StrictInverseFirstPower.cayleyToDisk_I line 78
  10. lemma OAI.StrictInverseFirstPower.cayleyToHalfPlane_zero line 79
  11. lemma OAI.StrictInverseFirstPower.cayleyToHalfPlane_toDisk line 81
  12. lemma OAI.StrictInverseFirstPower.cayleyToDisk_toHalfPlane line 89
  13. lemma OAI.StrictInverseFirstPower.cayleyToDisk_hasDerivAt line 97
  14. lemma OAI.StrictInverseFirstPower.cayleyToHalfPlane_hasDerivAt line 103
  15. lemma OAI.StrictInverseFirstPower.cayleyToDisk_differentiableOn line 110
  16. lemma OAI.StrictInverseFirstPower.cayleyToDisk_injOn line 114
  17. lemma OAI.StrictInverseFirstPower.cayleyToHalfPlane_injOn line 119
  18. def OAI.StrictInverseFirstPower.affineAt line 124
  19. lemma OAI.StrictInverseFirstPower.affineAt_im line 126
  20. lemma OAI.StrictInverseFirstPower.affineAt_re line 129
  21. lemma OAI.StrictInverseFirstPower.affineAt_mapsTo line 132
  22. lemma OAI.StrictInverseFirstPower.affineAt_injective line 137
  23. lemma OAI.StrictInverseFirstPower.affineAt_hasDerivAt line 141
  24. lemma OAI.StrictInverseFirstPower.affineAt_I line 146
  25. lemma OAI.StrictInverseFirstPower.affineAt_one line 148
  26. def OAI.StrictInverseFirstPower.affineProduct line 151
  27. lemma OAI.StrictInverseFirstPower.coe_affineProduct line 154
  28. lemma OAI.StrictInverseFirstPower.affineAt_assoc line 157
  29. lemma OAI.StrictInverseFirstPower.affineProduct_assoc line 167
  30. def OAI.StrictInverseFirstPower.affineInverse line 172
  31. lemma OAI.StrictInverseFirstPower.affineAt_inverse line 177
  32. def OAI.StrictInverseFirstPower.halfPlaneFunction line 192
  33. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_differentiableOn line 195
  34. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_injOn line 200
  35. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_I line 207
  36. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_hasDerivAt line 210
  37. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_deriv line 218
  38. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_deriv_I line 224
  39. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_deriv_ne_zero line 230
  40. def OAI.StrictInverseFirstPower.cayleyDiskMap line 237
  41. lemma OAI.StrictInverseFirstPower.continuous_halfPlaneFunction line 242
  42. lemma OAI.StrictInverseFirstPower.continuous_halfPlaneFunction_deriv line 252