OAI/Analysis/IntegralMeans/HalfPlane.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.halfPlane line 21
  2. lemma OAI.Brennan.isOpen_halfPlane line 23
  3. def OAI.Brennan.HalfPlaneSchlicht line 26
  4. def OAI.Brennan.affine line 29
  5. lemma OAI.Brennan.affine_I line 31
  6. lemma OAI.Brennan.I_affine line 34
  7. lemma OAI.Brennan.affine_assoc line 37
  8. lemma OAI.Brennan.affine_mem line 40
  9. lemma OAI.Brennan.affine_injective line 45
  10. lemma OAI.Brennan.hasDerivAt_affine line 50
  11. def OAI.Brennan.reroot line 54
  12. lemma OAI.Brennan.hasDerivAt_reroot line 57
  13. lemma OAI.Brennan.deriv_reroot line 68
  14. lemma OAI.Brennan.reroot_normalized line 73
  15. lemma OAI.Brennan.reroot_comp line 89
  16. def OAI.Brennan.reciprocalDeriv line 107
  17. lemma OAI.Brennan.reciprocalDeriv_reroot line 109
  18. def OAI.Brennan.diskCayley line 114
  19. def OAI.Brennan.halfCayley line 116
  20. lemma OAI.Brennan.cayley_den_ne_zero line 118
  21. lemma OAI.Brennan.halfCayley_den_ne_zero line 125
  22. lemma OAI.Brennan.diskCayley_maps line 131
  23. lemma OAI.Brennan.halfCayley_im line 146
  24. lemma OAI.Brennan.halfCayley_maps line 153
  25. lemma OAI.Brennan.halfCayley_diskCayley line 160
  26. lemma OAI.Brennan.diskCayley_halfCayley line 167
  27. lemma OAI.Brennan.diskCayley_hasDerivAt line 174
  28. lemma OAI.Brennan.halfCayley_hasDerivAt line 181
  29. lemma OAI.Brennan.diskCayley_I line 188
  30. lemma OAI.Brennan.halfCayley_zero line 190
  31. def OAI.Brennan.diskToHalf line 192
  32. def OAI.Brennan.halfToDisk line 194
  33. lemma OAI.Brennan.hasDerivAt_diskToHalf line 196
  34. lemma OAI.Brennan.hasDerivAt_halfToDisk line 205
  35. lemma OAI.Brennan.diskToHalf_schlicht line 213
  36. lemma OAI.Brennan.halfToDisk_schlicht line 224
  37. lemma OAI.Brennan.diskToHalf_halfToDisk line 235
  38. lemma OAI.Brennan.halfToDisk_diskToHalf line 240
  39. def OAI.Brennan.classFun line 244
  40. lemma OAI.Brennan.classFun_schlicht line 246
  41. def OAI.Brennan.classOfHalf line 249
  42. lemma OAI.Brennan.classFun_classOfHalf line 265
  43. lemma OAI.Brennan.continuous_classFun_eval line 272
  44. instance OAI.Brennan.(instance at line 281) line 281
  45. instance OAI.Brennan.(instance at line 283) line 283
  46. instance OAI.Brennan.(instance at line 285) line 285
  47. instance OAI.Brennan.(instance at line 287) line 287
  48. lemma OAI.Brennan.differentiableOn_iteratedDeriv_open line 289
  49. lemma OAI.Brennan.tendstoLocallyUniformlyOn_iteratedDeriv_open line 296
  50. def OAI.Brennan.classJet line 307
  51. lemma OAI.Brennan.continuous_classJet line 311
  52. lemma OAI.Brennan.continuous_classJet_eval line 324
  53. def OAI.Brennan.rerootClass line 328
  54. lemma OAI.Brennan.classFun_rerootClass line 331
  55. lemma OAI.Brennan.continuous_rerootClass line 335
  56. lemma OAI.Brennan.class_ext line 367
  57. lemma OAI.Brennan.reroot_congr line 378
  58. lemma OAI.Brennan.rerootClass_comp line 383
  59. def OAI.Brennan.classWeight line 390
  60. lemma OAI.Brennan.classWeight_pos line 392
  61. lemma OAI.Brennan.continuous_classWeight line 397
  62. lemma OAI.Brennan.classWeight_cocycle line 402