OAI/Geometry/Cannon/Beltrami/Increment.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonOrientation.simplyConnected_univ line 18
  2. lemma OAI.CannonOrientation.continuous_log_exists line 22
  3. lemma OAI.CannonOrientation.exp_equal_difference_constant line 31
  4. def OAI.CannonOrientation.HasIncrement line 43
  5. lemma OAI.CannonOrientation.HasIncrement.unique line 46
  6. lemma OAI.CannonOrientation.HasIncrement.of_homotopy line 53
  7. def OAI.CannonOrientation.circle line 68
  8. lemma OAI.CannonOrientation.continuous_circle line 70
  9. lemma OAI.CannonOrientation.norm_circle line 71
  10. lemma OAI.CannonOrientation.circle_ne_zero line 72
  11. lemma OAI.CannonOrientation.circle_zero line 73
  12. lemma OAI.CannonOrientation.circle_one line 74
  13. lemma OAI.CannonOrientation.increment_circle_mul line 76
  14. lemma OAI.CannonOrientation.increment_conj_circle_mul line 82
  15. def OAI.CannonOrientation.clip line 93
  16. lemma OAI.CannonOrientation.continuous_clip line 94
  17. lemma OAI.CannonOrientation.clip_nonneg line 95
  18. lemma OAI.CannonOrientation.clip_le_one line 96
  19. lemma OAI.CannonOrientation.clip_zero line 97
  20. lemma OAI.CannonOrientation.clip_one line 98
  21. lemma OAI.CannonOrientation.HasIncrement.mul_const line 105
  22. lemma OAI.CannonOrientation.HasIncrement.of_close line 114
  23. lemma OAI.CannonOrientation.increment_move_circle line 138
  24. lemma OAI.CannonOrientation.increment_at_derivative line 168
  25. theorem OAI.CannonOrientation.no_opposite_similarities line 195
  26. lemma OAI.CannonOrientation.conformal_scalar_cases line 215
  27. theorem OAI.CannonOrientation.conformal_differential_orientation line 233
  28. lemma OAI.CannonBeltrami.partialBar_reflect line 269
  29. def OAI.CannonBeltrami.barProject line 279
  30. lemma OAI.CannonBeltrami.barProject_apply line 282
  31. lemma OAI.CannonBeltrami.convolution_partialBar line 286
  32. lemma OAI.CannonBeltrami.weak_partialBar_convolution line 310
  33. lemma OAI.CannonBeltrami.mollify_eq_complex_convolution line 330
  34. lemma OAI.CannonBeltrami.mollifier_radius_tendsto line 338
  35. lemma OAI.CannonBeltrami.mollify_locally_uniform line 342
  36. theorem OAI.CannonBeltrami.weak_partialBar_zero_holomorphic line 355