Commit 2023-04-17 07:01 b000aad8

View on Github →

feat: port Dynamics.Circle.RotationNumber.TranslationNumber (#3433)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

added theorem CircleDeg1Lift.ceil_map_map_zero_le

added theorem CircleDeg1Lift.coe_mk

added theorem CircleDeg1Lift.coe_mul

added theorem CircleDeg1Lift.coe_one

added theorem CircleDeg1Lift.coe_pow

added theorem CircleDeg1Lift.coe_toOrderHom

added theorem CircleDeg1Lift.coe_toOrderIso

added theorem CircleDeg1Lift.coe_toOrderIso_inv

added theorem CircleDeg1Lift.coe_toOrderIso_symm

added theorem CircleDeg1Lift.commute_add_int

added theorem CircleDeg1Lift.commute_add_nat

added theorem CircleDeg1Lift.commute_iff_commute

added theorem CircleDeg1Lift.commute_int_add

added theorem CircleDeg1Lift.commute_nat_add

added theorem CircleDeg1Lift.commute_sub_int

added theorem CircleDeg1Lift.commute_sub_nat

added theorem CircleDeg1Lift.continuous_iff_surjective

added theorem CircleDeg1Lift.continuous_pow

added theorem CircleDeg1Lift.dist_map_map_zero_lt

added theorem CircleDeg1Lift.dist_map_zero_lt_of_semiconj

added theorem CircleDeg1Lift.dist_map_zero_lt_of_semiconjBy

added theorem CircleDeg1Lift.dist_map_zero_translationNumber_le

added theorem CircleDeg1Lift.dist_pow_map_zero_mul_translationNumber_le

added theorem CircleDeg1Lift.exists_eq_add_translationNumber

added theorem CircleDeg1Lift.ext

added theorem CircleDeg1Lift.ext_iff

added theorem CircleDeg1Lift.floor_map_map_zero_le

added theorem CircleDeg1Lift.floor_sub_le_translationNumber

added theorem CircleDeg1Lift.forall_map_sub_of_Icc

added theorem CircleDeg1Lift.inf_apply

added theorem CircleDeg1Lift.isUnit_iff_bijective

added theorem CircleDeg1Lift.iterate_eq_of_map_eq_add_int

added theorem CircleDeg1Lift.iterate_le_of_map_le_add_int

added theorem CircleDeg1Lift.iterate_mono

added theorem CircleDeg1Lift.iterate_monotone

added theorem CircleDeg1Lift.iterate_pos_eq_iff

added theorem CircleDeg1Lift.iterate_pos_le_iff

added theorem CircleDeg1Lift.iterate_pos_lt_iff

added theorem CircleDeg1Lift.le_ceil_map_map_zero

added theorem CircleDeg1Lift.le_floor_map_map_zero

added theorem CircleDeg1Lift.le_iterate_of_add_int_le_map

added theorem CircleDeg1Lift.le_iterate_pos_iff

added theorem CircleDeg1Lift.le_map_map_zero

added theorem CircleDeg1Lift.le_map_of_map_zero

added theorem CircleDeg1Lift.le_translationNumber_of_add_int_le

added theorem CircleDeg1Lift.le_translationNumber_of_add_le

added theorem CircleDeg1Lift.le_translationNumber_of_add_nat_le

added theorem CircleDeg1Lift.lt_iterate_pos_iff

added theorem CircleDeg1Lift.lt_map_map_zero

added theorem CircleDeg1Lift.lt_map_of_int_lt_translationNumber

added theorem CircleDeg1Lift.lt_map_of_nat_lt_translationNumber

added theorem CircleDeg1Lift.lt_translationNumber_of_forall_add_lt

added theorem CircleDeg1Lift.map_add_int

added theorem CircleDeg1Lift.map_add_nat

added theorem CircleDeg1Lift.map_add_one

added theorem CircleDeg1Lift.map_fract_sub_fract_eq

added theorem CircleDeg1Lift.map_int_add

added theorem CircleDeg1Lift.map_int_of_map_zero

added theorem CircleDeg1Lift.map_le_of_map_zero

added theorem CircleDeg1Lift.map_lt_add_floor_translationNumber_add_one

added theorem CircleDeg1Lift.map_lt_add_translationNumber_add_one

added theorem CircleDeg1Lift.map_lt_of_translationNumber_lt_int

added theorem CircleDeg1Lift.map_lt_of_translationNumber_lt_nat

added theorem CircleDeg1Lift.map_map_zero_le

added theorem CircleDeg1Lift.map_map_zero_lt

added theorem CircleDeg1Lift.map_nat_add

added theorem CircleDeg1Lift.map_one_add

added theorem CircleDeg1Lift.map_sub_int

added theorem CircleDeg1Lift.map_sub_nat

added theorem CircleDeg1Lift.mono

added theorem CircleDeg1Lift.mul_apply

added theorem CircleDeg1Lift.mul_floor_map_zero_le_floor_iterate_zero

added theorem CircleDeg1Lift.pow_mono

added theorem CircleDeg1Lift.pow_monotone

added theorem CircleDeg1Lift.semiconjBy_iff_semiconj

added theorem CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq

added theorem CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq

added theorem CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq

added theorem CircleDeg1Lift.strictMono_iff_injective

added theorem CircleDeg1Lift.sup_apply

added theorem CircleDeg1Lift.tendsto_translationNumber

added theorem CircleDeg1Lift.tendsto_translationNumber_aux

added theorem CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux

added theorem CircleDeg1Lift.tendsto_translation_number'

added theorem CircleDeg1Lift.tendsto_translation_number₀'

added theorem CircleDeg1Lift.tendsto_translation_number₀

added def CircleDeg1Lift.toOrderIso

added def CircleDeg1Lift.translate

added theorem CircleDeg1Lift.translate_apply

added theorem CircleDeg1Lift.translate_inv_apply

added theorem CircleDeg1Lift.translate_iterate

added theorem CircleDeg1Lift.translate_pow

added theorem CircleDeg1Lift.translate_zpow

added def CircleDeg1Lift.translationNumber

added theorem CircleDeg1Lift.translationNumber_conj_eq'

added theorem CircleDeg1Lift.translationNumber_conj_eq

added theorem CircleDeg1Lift.translationNumber_eq_int_iff

added theorem CircleDeg1Lift.translationNumber_eq_of_dist_bounded

added theorem CircleDeg1Lift.translationNumber_eq_of_semiconj

added theorem CircleDeg1Lift.translationNumber_eq_of_semiconjBy

added theorem CircleDeg1Lift.translationNumber_eq_of_tendsto_aux

added theorem CircleDeg1Lift.translationNumber_eq_of_tendsto₀'

added theorem CircleDeg1Lift.translationNumber_eq_of_tendsto₀

added theorem CircleDeg1Lift.translationNumber_eq_rat_iff

added theorem CircleDeg1Lift.translationNumber_le_ceil_sub

added theorem CircleDeg1Lift.translationNumber_le_of_le_add

added theorem CircleDeg1Lift.translationNumber_le_of_le_add_int

added theorem CircleDeg1Lift.translationNumber_le_of_le_add_nat

added theorem CircleDeg1Lift.translationNumber_lt_of_forall_lt_add

added theorem CircleDeg1Lift.translationNumber_mono

added theorem CircleDeg1Lift.translationNumber_mul_of_commute

added theorem CircleDeg1Lift.translationNumber_of_eq_add_int

added theorem CircleDeg1Lift.translationNumber_of_map_pow_eq_add_int

added theorem CircleDeg1Lift.translationNumber_one

added theorem CircleDeg1Lift.translationNumber_pow

added theorem CircleDeg1Lift.translationNumber_translate

added theorem CircleDeg1Lift.translationNumber_units_inv

added theorem CircleDeg1Lift.translationNumber_zpow

added def CircleDeg1Lift.transnumAuxSeq

added theorem CircleDeg1Lift.transnumAuxSeq_def

added theorem CircleDeg1Lift.transnumAuxSeq_dist_lt

added theorem CircleDeg1Lift.transnumAuxSeq_zero

added theorem CircleDeg1Lift.units_apply_inv_apply

added theorem CircleDeg1Lift.units_inv_apply_apply

added theorem CircleDeg1Lift.units_semiconj_of_translationNumber_eq

added structure CircleDeg1Lift