Derivatives of lifts of circle maps

A map of the circle AddCircle T of degree one is described by a lift F : ℝ → ℝ with F (x + T) = F x + T (see TauCeti.Topology.Instances.AddCircle.Lift). The derivative of a differentiable lift is T-periodic, so a lift with continuous positive derivative, the lift of an orientation-preserving C¹ diffeomorphism, has derivative bounded between two positive constants, and its inverse is again a lift, with derivative the reciprocal of F'. A bound on the derivative of a lift is a Lipschitz constant of the circle map for the quotient metric.

Main declarations

• AddCircle.periodic_deriv_of_lift: the derivative of a lift is T-periodic.
• AddCircle.derivOfLift: the derivative F' of a lift, as a continuous complex function on the circle; it is smooth when F' is (AddCircle.contDiff_derivOfLift).
• AddCircle.hasDerivAt_add_mul_sub, AddCircle.one_sub_add_mul_pos: for a weight c ∈ [0, 1], the interpolation x ↦ x + c * (F x - x) between the identity and a lift F with F' > 0 (again a lift, AddCircle.add_mul_sub_add_period) has positive derivative.
• AddCircle.exists_pos_le_deriv_le_of_lift: a lift with continuous positive derivative has derivative in some interval [c, M] with 0 < c.
• AddCircle.exists_lift_inverse: a lift with positive derivative has an inverse G, which is again a lift, with derivative G' y = (F' (G y))⁻¹.
• AddCircle.exists_inverse_of_lift: the inverse map of a circle map whose lift has derivative in [c, M], 0 < c, with a lift whose derivative lies in [M⁻¹, c⁻¹].
• AddCircle.lipschitzWith_of_lift: a lift with derivative bounded by C in norm gives a C-Lipschitz map of the circle; in particular a lift with derivative in [0, M] gives an M-Lipschitz map (AddCircle.lipschitzWith_toNNReal_of_lift).

theorem AddCircle.periodic_deriv_of_lift {T : ℝ} {F F' : ℝ → ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) : Function.Periodic F' T

The derivative of a lift F with F (x + T) = F x + T is T-periodic.

noncomputable def AddCircle.derivOfLift {T : ℝ} {F F' : ℝ → ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hF'c : Continuous F') : C(AddCircle T, ℂ)

The derivative F' of a lift F, F (x + T) = F x + T, regarded as a continuous complex function on the circle; it is well defined since F' is T-periodic (AddCircle.periodic_deriv_of_lift).

@[simp]

theorem AddCircle.derivOfLift_coe {T : ℝ} {F F' : ℝ → ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hF'c : Continuous F') (x : ℝ) : (derivOfLift hF hper hF'c) ↑x = ↑(F' x)

theorem AddCircle.eq_derivOfLift_of_coe {T : ℝ} {F F' : ℝ → ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hF'c : Continuous F') {f' : AddCircle T → ℂ} (hf' : ∀ (x : ℝ), f' ↑x = ↑(F' x)) : f' = ⇑(derivOfLift hF hper hF'c)

A function on the circle which agrees with the derivative F' of a lift on every point of ℝ is AddCircle.derivOfLift.

theorem AddCircle.derivOfLift_ne_zero {T : ℝ} {F F' : ℝ → ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) {c : ℝ} (hc : 0 < c) (hcF : ∀ (x : ℝ), c ≤ F' x) (hF'c : Continuous F') (y : AddCircle T) : (derivOfLift hF hper hF'c) y ≠ 0

The derivative of a lift with 0 < c ≤ F' does not vanish on the circle.

theorem AddCircle.contDiff_derivOfLift {T : ℝ} {F F' : ℝ → ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hF' : ContDiff ℝ (↑⊤) F') (hF'c : Continuous F') : ContDiff ℝ ↑⊤ fun (x : ℝ) => (derivOfLift hF hper hF'c) ↑x

The derivative of a lift with smooth derivative is a smooth function on the circle.

theorem AddCircle.hasDerivAt_add_mul_sub {F : ℝ → ℝ} {f' x : ℝ} (hF : HasDerivAt F f' x) (c : ℝ) : HasDerivAt (fun (y : ℝ) => y + c * (F y - y)) (1 - c + c * f') x

The interpolation x ↦ x + c * (F x - x) between the identity and F has derivative 1 - c + c * F' wherever F has derivative F'.

theorem AddCircle.one_sub_add_mul_pos {c f' : ℝ} (hc₀ : 0 ≤ c) (hc₁ : c ≤ 1) (hf' : 0 < f') : 0 < 1 - c + c * f'

For a weight c ∈ [0, 1] and a positive derivative f' of a lift, the derivative 1 - c + c * f' of the interpolating lift (AddCircle.hasDerivAt_add_mul_sub) is positive.

theorem AddCircle.exists_pos_le_deriv_le_of_lift {T : ℝ} {F F' : ℝ → ℝ} [hT : Fact (0 < T)] (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hF' : Continuous F') (hpos : ∀ (x : ℝ), 0 < F' x) : ∃ (c : ℝ) (M : ℝ), 0 < c ∧ (∀ (x : ℝ), c ≤ F' x) ∧ ∀ (x : ℝ), F' x ≤ M

A lift with continuous positive derivative has derivative bounded above and below by positive constants: a C¹ lift of an orientation-preserving diffeomorphism of the circle has derivative in some [c, M] with 0 < c.

theorem AddCircle.exists_lift_inverse {T : ℝ} {F F' : ℝ → ℝ} [hT : Fact (0 < T)] (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < F' x) : ∃ (G : ℝ → ℝ), Function.LeftInverse G F ∧ Function.RightInverse G F ∧ (∀ (y : ℝ), G (y + T) = G y + T) ∧ ∀ (y : ℝ), HasDerivAt G (F' (G y))⁻¹ y

The inverse of a lift. A lift F with F (x + T) = F x + T and positive derivative F' is a bijection of ℝ. Its inverse G is again a lift, G (y + T) = G y + T, and it is differentiable with G' y = (F' (G y))⁻¹. So the inverse of an orientation-preserving diffeomorphism of the circle with lift F has the lift G.

theorem AddCircle.exists_inverse_of_lift {T : ℝ} {F F' : ℝ → ℝ} [hT : Fact (0 < T)] {φ : AddCircle T → AddCircle T} {c M : ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) (hc : 0 < c) (hcF : ∀ (x : ℝ), c ≤ F' x) (hMF : ∀ (x : ℝ), F' x ≤ M) : ∃ (ψ : AddCircle T → AddCircle T) (G : ℝ → ℝ), Function.LeftInverse ψ φ ∧ Function.LeftInverse G F ∧ Function.RightInverse G F ∧ (∀ (y : ℝ), G (y + T) = G y + T) ∧ (∀ (y : ℝ), ψ ↑y = ↑(G y)) ∧ (∀ (y : ℝ), HasDerivAt G (F' (G y))⁻¹ y) ∧ (∀ (y : ℝ), M⁻¹ ≤ (F' (G y))⁻¹) ∧ ∀ (y : ℝ), (F' (G y))⁻¹ ≤ c⁻¹

The inverse of a circle map with a lift. Let φ have the lift F, φ x = F x with F (x + T) = F x + T, and derivative 0 < c ≤ F' ≤ M. Then φ has a left inverse ψ with the lift G, the inverse of F (AddCircle.exists_lift_inverse). The derivative G' = (F' ∘ G)⁻¹ lies between M⁻¹ and c⁻¹.

theorem AddCircle.lipschitzWith_of_lift {T : ℝ} {F F' : ℝ → ℝ} {φ : AddCircle T → AddCircle T} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) {C : NNReal} (hC : ∀ (x : ℝ), ‖F' x‖₊ ≤ C) : LipschitzWith C φ

A bound on the derivative of a lift is a Lipschitz constant. If the lift F of φ, φ x = F x, has derivative bounded by C in norm, then φ is C-Lipschitz for the quotient metric of the circle.

theorem AddCircle.lipschitzWith_toNNReal_of_lift {T : ℝ} {F F' : ℝ → ℝ} {φ : AddCircle T → AddCircle T} {M : ℝ} (hF : ∀ (x : ℝ), HasDerivAt F (F' x) x) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) (h0F : ∀ (x : ℝ), 0 ≤ F' x) (hMF : ∀ (x : ℝ), F' x ≤ M) : LipschitzWith M.toNNReal φ

A map of the circle with lift F, φ x = F x, and derivative 0 ≤ F' ≤ M is M-Lipschitz for the quotient metric of the circle.