CircleDeg1Lift.translationNumber_pow
theorem CircleDeg1Lift.translationNumber_pow :
∀ (f : CircleDeg1Lift) (n : ℕ), (f ^ n).translationNumber = ↑n * f.translationNumber
The theorem `CircleDeg1Lift.translationNumber_pow` states that for any `CircleDeg1Lift` function `f` and any natural number `n`, the translation number of the `n`-th power of `f` is equal to `n` multiplied by the translation number of the original function `f`. In mathematical terms, if τ(f) denotes the translation number of function `f`, then for all `f : CircleDeg1Lift` and `n : ℕ`, we have τ(f^n) = n * τ(f).
More concisely: The translation number of a `CircleDeg1Lift` function raised to the power of a natural number is equal to the product of that number and the translation number of the original function.
|
CircleDeg1Lift.mono
theorem CircleDeg1Lift.mono : ∀ (f : CircleDeg1Lift) {x y : ℝ}, x ≤ y → f x ≤ f y
This theorem states that for any function `f` of type `CircleDeg1Lift` and for any real numbers `x` and `y`, if `x` is less than or equal to `y`, then `f(x)` is less than or equal to `f(y)`. In other words, the function `f` is monotonic: it preserves or increases the order of its inputs.
More concisely: For any function `f` of type `CircleDeg1Lift`, if `x <= y` then `f x <= f y`.
|
CircleDeg1Lift.le_translationNumber_of_add_int_le
theorem CircleDeg1Lift.le_translationNumber_of_add_int_le :
∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, x + ↑m ≤ f x → ↑m ≤ f.translationNumber
The theorem `CircleDeg1Lift.le_translationNumber_of_add_int_le` states that for any transformation `f` represented by the type `CircleDeg1Lift`, any real number `x`, and any integer `m`, if `x` plus the real representation of `m` is less than or equal to the value of `f` at `x`, then the real representation of `m` is less than or equal to the translation number of `f`. In mathematical terms, for all `f`, `x`, and `m`, if $x + m \leq f(x)$ then $m \leq τ(f)$, where $τ(f)$ represents the translation number of `f`.
More concisely: If $x + m \leq f(x)$ for a transformation $f$ and real numbers $x$ and $m$, then $m \leq τ(f)$, where $τ(f)$ is the translation number of $f$.
|
CircleDeg1Lift.exists_eq_add_translationNumber
theorem CircleDeg1Lift.exists_eq_add_translationNumber :
∀ (f : CircleDeg1Lift), Continuous ⇑f → ∃ x, f x = x + f.translationNumber
This theorem states that for any function `f`, which is a continuous monotone map from the real numbers to the real numbers and satisfies the property `f (x + 1) = f x + 1`, there exists a real number `x` such that the value of `f` at `x` is equal to `x` plus the translation number of `f`. The translation number of a function is a measure of the average amount that the function shifts points in the domain.
More concisely: Given a continuous, monotone function `f` with the property `f (x + 1) = f x + 1`, there exists a real number `x` such that `f x = x + trans (f)`, where `trans (f)` denotes the translation number of `f`.
|
CircleDeg1Lift.le_map_map_zero
theorem CircleDeg1Lift.le_map_map_zero : ∀ (f g : CircleDeg1Lift), f 0 + ↑⌊g 0⌋ ≤ f (g 0)
This theorem states that for any two functions `f` and `g` of type `CircleDeg1Lift`, the sum of the output of `f` at zero and the integer part of the output of `g` at zero is always less than or equal to the output of `f` at the point where `g` outputs zero. In mathematical terms, for all `f` and `g`, we have `f(0) + ⌊g(0)⌋ ≤ f(g(0))`.
More concisely: For all functions `f` and `g` of type `CircleDeg1Lift`, the relationship `f(0) + ⌊g(0)⌋ ≤ f(g(0))` holds.
|
CircleDeg1Lift.commute_add_int
theorem CircleDeg1Lift.commute_add_int : ∀ (f : CircleDeg1Lift) (n : ℤ), Function.Commute ⇑f fun x => x + ↑n
The theorem `CircleDeg1Lift.commute_add_int` states that for any `CircleDeg1Lift` function `f` and any integer `n`, the function `f` commutes with the function that adds `n` to its input. In other words, applying `f` and then adding `n` is the same as first adding `n` and then applying `f` for all inputs, expressed mathematically as `f(x + n) = f(x) + n` for all `x`.
More concisely: For all `CircleDeg1Lift` functions `f` and integers `n`, `f(x + n) = f(x) + n` for all `x`.
|
CircleDeg1Lift.ext
theorem CircleDeg1Lift.ext : ∀ ⦃f g : CircleDeg1Lift⦄, (∀ (x : ℝ), f x = g x) → f = g
This theorem, named `CircleDeg1Lift.ext`, states that for any two objects `f` and `g` of type `CircleDeg1Lift`, if for all real numbers `x`, the application of `f` to `x` is equal to the application of `g` to `x`, then `f` and `g` are equal. In other words, two `CircleDeg1Lift` functions are equal if they produce the same results for all real numbers.
More concisely: If two functions `f` and `g` in the type `CircleDeg1Lift` agree on all real numbers, then they are equal.
|
CircleDeg1Lift.coe_pow
theorem CircleDeg1Lift.coe_pow : ∀ (f : CircleDeg1Lift) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
This theorem states that for any function `f` of type `CircleDeg1Lift` and any natural number `n`, applying the function `f` `n` times (denoted as `f ^ n`) is the same as the `n`-th iteration of the function `f` (denoted as `(⇑f)^[n]`). In other words, multiplying `f` by itself `n` times (i.e., composing `f` with itself `n` times) yields the same result as applying `f` `n` times in sequence.
More concisely: For any function `f` of type `CircleDeg1Lift` in Lean 4, `(f ^ n) = (⇑f)^[n]` or equivalently, `f ^ n = (composition f f ... f) (n times) = (iterated function application f) (n times)`.
|
CircleDeg1Lift.forall_map_sub_of_Icc
theorem CircleDeg1Lift.forall_map_sub_of_Icc :
∀ (f : CircleDeg1Lift) (P : ℝ → Prop), (∀ x ∈ Set.Icc 0 1, P (f x - x)) → ∀ (x : ℝ), P (f x - x)
This theorem states that for any Circle Degree 1 Lift function `f` and any real-valued predicate `P`, if the predicate `P` holds for all `x` in the closed interval from 0 to 1 (i.e., `0 ≤ x ≤ 1`) considering the difference `f(x) - x`, then it can be concluded that the predicate `P` holds for the difference `f(x) - x` for all real numbers `x`. In other words, if a property about the difference between a Circle Degree 1 Lift function at `x` and `x` itself is true for `x` between 0 and 1, then this property is true for all real `x`.
More concisely: If a real-valued predicate holds for the difference between a Circle Degree 1 Lift function and its argument on the interval [0, 1], then it holds for the difference between the function and its argument for all real numbers.
|
CircleDeg1Lift.translationNumber_of_eq_add_int
theorem CircleDeg1Lift.translationNumber_of_eq_add_int :
∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, f x = x + ↑m → f.translationNumber = ↑m
The theorem `CircleDeg1Lift.translationNumber_of_eq_add_int` states that for any function `f` of type `CircleDeg1Lift` and any real number `x`, if the result of applying `f` to `x` equals `x` plus some integer `m` (i.e., `f x = x + m`), then the translation number of `f` is equal to `m`. In the context of circular motion, this implies that a map with a fixed point has a rotation number of zero.
More concisely: If a CircleDeg1Lift function `f` satisfies `f x = x + m` for some integer `m`, then the translation number of `f` equals `m`.
|
CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq
theorem CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq :
∀ {f₁ f₂ : CircleDeg1Lift},
Function.Bijective ⇑f₁ →
Function.Bijective ⇑f₂ → f₁.translationNumber = f₂.translationNumber → ∃ F, Function.Semiconj ⇑F ⇑f₁ ⇑f₂
The theorem `CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq` states that for any two lifts of circle homeomorphisms, denoted as `f₁` and `f₂`, if both these lifts are bijective functions (i.e., they are both injective and surjective), and they have the same translation number, then there exists a lift of a circle homeomorphism, denoted as `F`, which semiconjugates `f₁` to `f₂`. Here, to "semiconjugate" means that the composition of `F` and `f₁` is equal to the composition of `f₂` and `F` for all elements in the domain. In other words, for any element `x`, applying `f₁` to `x` and then applying `F` gives the same result as applying `F` to `x` and then applying `f₂`.
More concisely: If two bijective circle homeomorphism lifts have equal translation numbers, then there exists a third bijective lift that semiconjugates the first to the second.
|
CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq
theorem CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq :
∀ {f₁ f₂ : CircleDeg1Lift},
IsUnit f₁ → IsUnit f₂ → f₁.translationNumber = f₂.translationNumber → ∃ F, Function.Semiconj ⇑F ⇑f₁ ⇑f₂
This theorem states that if we have two lifts of circle homeomorphisms, say `f₁` and `f₂`, and both are units (which implies that `f₁` and `f₂` are homeomorphisms), then if these two lifts have the same translation number, there exists a `CircleDeg1Lift` `F` such that `F` semiconjugates `f₁` to `f₂`. In other words, applying `F` after `f₁` is the same as applying `f₂` after `F` for all points on the circle.
More concisely: If two unit circle homeomorphisms `f₁` and `f₂` have the same translation number, then there exists a `CircleDeg1Lift` `F` such that `f₁ ∘ F = F ∘ f₂`.
|
CircleDeg1Lift.translationNumber_le_of_le_add_int
theorem CircleDeg1Lift.translationNumber_le_of_le_add_int :
∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, f x ≤ x + ↑m → f.translationNumber ≤ ↑m
This theorem states that for any instance 'f' of the type 'CircleDeg1Lift' and for any real number 'x' and integer 'm', if 'f x' is less than or equal to 'x' plus the real part of 'm', then the translation number of 'f' is less than or equal to the real part of 'm'. Here, the translation number of a 'CircleDeg1Lift', denoted by 'τ(f)', is defined as the limit of the sequence 'f^{2^n}(0) / 2^n' as 'n' approaches infinity.
More concisely: For any 'CircleDeg1Lift' function 'f' and real numbers 'x' and 'm', if 'f(x) ≤ x + Re(m)' then 'τ(f) ≤ Re(m)'. Here, 'τ(f)' is the limit of 'f(0).2^n / 2^n' as 'n' approaches infinity.
|
CircleDeg1Lift.translationNumber_of_map_pow_eq_add_int
theorem CircleDeg1Lift.translationNumber_of_map_pow_eq_add_int :
∀ (f : CircleDeg1Lift) {x : ℝ} {n : ℕ} {m : ℤ}, (f ^ n) x = x + ↑m → 0 < n → f.translationNumber = ↑m / ↑n := by
sorry
This theorem states that if a function `f` raised to the power `n` and applied to some real number `x` minus `x` gives an integer `m`, where `n` is greater than 0, then the translation number of the function `f` is `m / n`. In the context of the circle, this implies that any map with a periodic orbit has a rational rotation number.
More concisely: Given a real function `f` and integer `m` such that `(f^n(x) - x)` equals `m` for some real number `x` and positive integer `n`, then the rotation number of `f` is `rational` with denominator `n`, i.e., `rationals.exists (denom: ℕ) (rational.num r := m / n) (rational.denom r := denom)`.
|
CircleDeg1Lift.tendsto_translationNumber
theorem CircleDeg1Lift.tendsto_translationNumber :
∀ (f : CircleDeg1Lift) (x : ℝ),
Filter.Tendsto (fun n => ((f ^ n) x - x) / ↑n) Filter.atTop (nhds f.translationNumber)
The theorem `CircleDeg1Lift.tendsto_translationNumber` states that for any real number `x` and any `f` of type `CircleDeg1Lift`, the sequence defined by `(f^n(x) - x) / n` tends to the translation number of `f` as `n` goes to infinity. In other words, the limit of this sequence is the translation number of `f` and this limit does not depend on the initial real number `x`. Here, `f^n(x)` means applying the function `f` `n` times to `x`, and `f.translationNumber` is the translation number of `f`. The filter `Filter.atTop` represents the limit going to infinity, and `nhds f.translationNumber` is the neighborhood filter at the translation number of `f`, which is a way to represent taking a limit at a particular value.
More concisely: For any real number `x` and function `f` of type `CircleDeg1Lift`, the sequence `((f^n(x) - x) / n)` converges to `f.translationNumber` as `n` approaches infinity, regardless of the choice of `x`.
|
CircleDeg1Lift.monotone
theorem CircleDeg1Lift.monotone : ∀ (f : CircleDeg1Lift), Monotone ⇑f
The theorem `CircleDeg1Lift.monotone` asserts that for every function `f` of type `CircleDeg1Lift`, `f` is monotonic. In terms of mathematics, this means that for every function `f` from the type `CircleDeg1Lift`, if `a` is less than or equal to `b` then `f(a)` is less than or equal to `f(b)`. This property is true for all `a` and `b` in the domain of `f`.
More concisely: For every function `f` in `CircleDeg1Lift`, if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`.
|
CircleDeg1Lift.map_map_zero_le
theorem CircleDeg1Lift.map_map_zero_le : ∀ (f g : CircleDeg1Lift), f (g 0) ≤ f 0 + ↑⌈g 0⌉
This theorem states that for any two Circle Degree 1 Lift functions `f` and `g`, the value of function `f` at the point `g 0` is less than or equal to the sum of the value of function `f` at 0 and the ceiling of the value of `g` at 0. In mathematical terms, for all `f` and `g`, we have `f(g(0)) ≤ f(0) + ⌈g(0)⌉`. The Circle Degree 1 Lift is a mathematical concept often used in complex analysis and dynamical systems.
More concisely: For any Circle Degree 1 Lift functions f and g, the value of f at g(0) is less than or equal to the sum of f(0) and the ceiling of g(0).
|
CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq
theorem CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq :
∀ {G : Type u_1} [inst : Group G] (f₁ f₂ : G →* CircleDeg1Lift),
(∀ (g : G), (f₁ g).translationNumber = (f₂ g).translationNumber) →
∃ F, ∀ (g : G), Function.Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
This theorem states that given two action functions `f₁` and `f₂` of a group `G` on the real line via lifts of orientation-preserving circle homeomorphisms, if for every element `g` of the group `G`, the homeomorphisms `f₁ g` and `f₂ g` have the same rotation numbers, then there exists a function `F` from the space of orientation-preserving circle homeomorphisms, such that `F` semiconjugates `f₁ g` to `f₂ g` for all `g` in `G`. Here, a function `F` is said to semiconjugate `f₁ g` to `f₂ g` if the composition of `F` with `f₁ g` equals the composition of `f₂ g` with `F`. This is a version of Proposition 5.4 from Étienne Ghys' work, "Groupes d'homeomorphismes du cercle et cohomologie bornee".
More concisely: Given two group actions on the real line by orientation-preserving circle homeomorphisms with equal rotation numbers for each group element, there exists a semiconjugacy between the actions.
|
CircleDeg1Lift.map_add_one
theorem CircleDeg1Lift.map_add_one : ∀ (f : CircleDeg1Lift) (x : ℝ), f (x + 1) = f x + 1
This theorem states that for any Circle Degree 1 Lift `f` and any real number `x`, the function `f` applied to `(x + 1)` is equal to `f x + 1`. In other words, adding 1 to the input of the Circle Degree 1 Lift function is equivalent to adding 1 to the output of the function when applied to the original input.
More concisely: For any Circle Degree 1 Lift function $f$ and real number $x$, we have $f(x+1) = f(x) + 1$.
|
CircleDeg1Lift.units_semiconj_of_translationNumber_eq
theorem CircleDeg1Lift.units_semiconj_of_translationNumber_eq :
∀ {f₁ f₂ : CircleDeg1Liftˣ},
(↑f₁).translationNumber = (↑f₂).translationNumber → ∃ F, Function.Semiconj ⇑F ⇑↑f₁ ⇑↑f₂
This theorem states that if two lifts of circle homeomorphisms, denoted as `f₁` and `f₂`, have the same translation number, then there exists a function `F` which is a `CircleDeg1Lift` such that `F` semiconjugates `f₁` to `f₂`. Here, a function `f` semiconjugates `ga` to `gb` if the composition of `f` and `ga` is equal to the composition of `gb` and `f`, for all `x` in the domain of `ga` and `gb`. In other words, it means `f(ga(x)) = gb(f(x))` for all `x`.
More concisely: If two liftings `f₁` and `f₂` of circle homeomorphisms have the same translation number, then there exists a `CircleDeg1Lift` function `F` such that `F` semiconjugates `f₁` and `f₂`.
|