Commit 2020-06-08 07:00 592f769e

View on Github →

feat(dynamics/circle): define translation number of a lift of a circle homeo (#2974) Define a structure circle_deg1_lift, a function translation_number : circle_deg1_lift → ℝ, and prove some basic properties

Estimated changes

Modified src/algebra/semiconj.lean

deleted theorem semiconj_by.units_conj_mk

added theorem units.conj_pow'

added theorem units.conj_pow

added theorem units.mk_semiconj_by

Created src/dynamics/circle/rotation_number/translation_number.lean

added theorem circle_deg1_lift.ceil_map_map_zero_le

added theorem circle_deg1_lift.coe_inj

added theorem circle_deg1_lift.coe_mk

added theorem circle_deg1_lift.coe_mul

added theorem circle_deg1_lift.coe_one

added theorem circle_deg1_lift.coe_pow

added theorem circle_deg1_lift.commute_add_int

added theorem circle_deg1_lift.commute_add_nat

added theorem circle_deg1_lift.commute_iff_commute

added theorem circle_deg1_lift.commute_int_add

added theorem circle_deg1_lift.commute_nat_add

added theorem circle_deg1_lift.commute_sub_int

added theorem circle_deg1_lift.commute_sub_nat

added theorem circle_deg1_lift.continuous_pow

added theorem circle_deg1_lift.dist_map_map_zero_lt

added theorem circle_deg1_lift.dist_map_zero_lt_of_semiconj

added theorem circle_deg1_lift.dist_map_zero_lt_of_semiconj_by

added theorem circle_deg1_lift.dist_map_zero_translation_number_le

added theorem circle_deg1_lift.dist_pow_map_zero_mul_translation_number_le

added theorem circle_deg1_lift.exists_eq_add_translation_number

added theorem circle_deg1_lift.ext

added theorem circle_deg1_lift.ext_iff

added theorem circle_deg1_lift.floor_map_map_zero_le

added theorem circle_deg1_lift.floor_sub_le_translation_number

added theorem circle_deg1_lift.forall_map_sub_of_Icc

added theorem circle_deg1_lift.inf_apply

added theorem circle_deg1_lift.iterate_eq_of_map_eq_add_int

added theorem circle_deg1_lift.iterate_le_of_map_le_add_int

added theorem circle_deg1_lift.iterate_mono

added theorem circle_deg1_lift.iterate_monotone

added theorem circle_deg1_lift.iterate_pos_eq_iff

added theorem circle_deg1_lift.iterate_pos_le_iff

added theorem circle_deg1_lift.iterate_pos_lt_iff

added theorem circle_deg1_lift.le_ceil_map_map_zero

added theorem circle_deg1_lift.le_floor_map_map_zero

added theorem circle_deg1_lift.le_iterate_of_add_int_le_map

added theorem circle_deg1_lift.le_iterate_pos_iff

added theorem circle_deg1_lift.le_map_map_zero

added theorem circle_deg1_lift.le_map_of_map_zero

added theorem circle_deg1_lift.le_translation_number_of_add_int_le

added theorem circle_deg1_lift.le_translation_number_of_add_le

added theorem circle_deg1_lift.le_translation_number_of_add_nat_le

added theorem circle_deg1_lift.lt_iterate_pos_iff

added theorem circle_deg1_lift.lt_map_map_zero

added theorem circle_deg1_lift.lt_map_of_int_lt_translation_number

added theorem circle_deg1_lift.lt_map_of_nat_lt_translation_number

added theorem circle_deg1_lift.lt_translation_number_of_forall_add_lt

added theorem circle_deg1_lift.map_add_int

added theorem circle_deg1_lift.map_add_nat

added theorem circle_deg1_lift.map_add_one

added theorem circle_deg1_lift.map_fract_sub_fract_eq

added theorem circle_deg1_lift.map_int_add

added theorem circle_deg1_lift.map_int_of_map_zero

added theorem circle_deg1_lift.map_le_of_map_zero

added theorem circle_deg1_lift.map_lt_of_translation_number_lt_int

added theorem circle_deg1_lift.map_lt_of_translation_number_lt_nat

added theorem circle_deg1_lift.map_map_zero_le

added theorem circle_deg1_lift.map_map_zero_lt

added theorem circle_deg1_lift.map_nat_add

added theorem circle_deg1_lift.map_one_add

added theorem circle_deg1_lift.map_sub_int

added theorem circle_deg1_lift.map_sub_nat

added theorem circle_deg1_lift.mono

added theorem circle_deg1_lift.mul_apply

added theorem circle_deg1_lift.mul_floor_map_zero_le_floor_iterate_zero

added theorem circle_deg1_lift.pow_mono

added theorem circle_deg1_lift.pow_monotone

added theorem circle_deg1_lift.semiconj_by_iff_semiconj

added theorem circle_deg1_lift.sup_apply

added theorem circle_deg1_lift.tendsto_translation_number'

added theorem circle_deg1_lift.tendsto_translation_number

added theorem circle_deg1_lift.tendsto_translation_number_aux

added theorem circle_deg1_lift.tendsto_translation_number_of_dist_bounded_aux

added theorem circle_deg1_lift.tendsto_translation_number₀'

added theorem circle_deg1_lift.tendsto_translation_number₀

added def circle_deg1_lift.translate

added theorem circle_deg1_lift.translate_apply

added theorem circle_deg1_lift.translate_gpow

added theorem circle_deg1_lift.translate_inv_apply

added theorem circle_deg1_lift.translate_iterate

added theorem circle_deg1_lift.translate_pow

added def circle_deg1_lift.translation_number

added theorem circle_deg1_lift.translation_number_conj_eq'

added theorem circle_deg1_lift.translation_number_conj_eq

added theorem circle_deg1_lift.translation_number_eq_int_iff

added theorem circle_deg1_lift.translation_number_eq_of_dist_bounded

added theorem circle_deg1_lift.translation_number_eq_of_semiconj

added theorem circle_deg1_lift.translation_number_eq_of_semiconj_by

added theorem circle_deg1_lift.translation_number_eq_of_tendsto_aux

added theorem circle_deg1_lift.translation_number_eq_of_tendsto₀'

added theorem circle_deg1_lift.translation_number_eq_of_tendsto₀

added theorem circle_deg1_lift.translation_number_eq_rat_iff

added theorem circle_deg1_lift.translation_number_le_ceil_sub

added theorem circle_deg1_lift.translation_number_le_of_le_add

added theorem circle_deg1_lift.translation_number_le_of_le_add_int

added theorem circle_deg1_lift.translation_number_le_of_le_add_nat

added theorem circle_deg1_lift.translation_number_lt_of_forall_lt_add

added theorem circle_deg1_lift.translation_number_map_id

added theorem circle_deg1_lift.translation_number_mono

added theorem circle_deg1_lift.translation_number_mul_of_commute

added theorem circle_deg1_lift.translation_number_of_eq_add_int

added theorem circle_deg1_lift.translation_number_of_map_pow_eq_add_int

added theorem circle_deg1_lift.translation_number_pow

added theorem circle_deg1_lift.translation_number_translate

added def circle_deg1_lift.transnum_aux_seq

added theorem circle_deg1_lift.transnum_aux_seq_def

added theorem circle_deg1_lift.transnum_aux_seq_dist_lt

added theorem circle_deg1_lift.transnum_aux_seq_zero

added theorem circle_deg1_lift.units_coe

added structure circle_deg1_lift