Commit 2023-06-28 13:56 6726709b

View on Github →

feat: port Analysis.Complex.UpperHalfPlane.Metric (#5544)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

added def UpperHalfPlane.center

added theorem UpperHalfPlane.center_im

added theorem UpperHalfPlane.center_re

added theorem UpperHalfPlane.center_zero

added theorem UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center

added theorem UpperHalfPlane.cosh_dist'

added theorem UpperHalfPlane.cosh_dist

added theorem UpperHalfPlane.cosh_half_dist

added theorem UpperHalfPlane.dist_center_dist

added theorem UpperHalfPlane.dist_coe_center

added theorem UpperHalfPlane.dist_coe_center_sq

added theorem UpperHalfPlane.dist_coe_le

added theorem UpperHalfPlane.dist_eq

added theorem UpperHalfPlane.dist_eq_iff_dist_coe_center_eq

added theorem UpperHalfPlane.dist_eq_iff_eq_sinh

added theorem UpperHalfPlane.dist_eq_iff_eq_sq_sinh

added theorem UpperHalfPlane.dist_le_dist_coe_div_sqrt

added theorem UpperHalfPlane.dist_le_iff_dist_coe_center_le

added theorem UpperHalfPlane.dist_le_iff_le_sinh

added theorem UpperHalfPlane.dist_log_im_le

added theorem UpperHalfPlane.dist_lt_iff_dist_coe_center_lt

added theorem UpperHalfPlane.dist_self_center

added theorem UpperHalfPlane.exp_half_dist

added theorem UpperHalfPlane.im_div_exp_dist_le

added theorem UpperHalfPlane.im_le_im_mul_exp_dist

added theorem UpperHalfPlane.im_pos_of_dist_center_le

added theorem UpperHalfPlane.image_coe_ball

added theorem UpperHalfPlane.image_coe_closedBall

added theorem UpperHalfPlane.image_coe_sphere

added theorem UpperHalfPlane.isometry_pos_mul

added theorem UpperHalfPlane.isometry_real_vadd

added theorem UpperHalfPlane.isometry_vertical_line

added theorem UpperHalfPlane.le_dist_coe

added theorem UpperHalfPlane.le_dist_iff_le_dist_coe_center

added theorem UpperHalfPlane.lt_dist_iff_lt_dist_coe_center

added def UpperHalfPlane.metricSpaceAux

added theorem UpperHalfPlane.sinh_half_dist

added theorem UpperHalfPlane.sinh_half_dist_add_dist

added theorem UpperHalfPlane.tanh_half_dist