Extending a diffeomorphism of the circle over the disc

An orientation-preserving diffeomorphism σ of the unit circle is described by a lift F : ℝ → ℝ, σ (Circle.exp x) = Circle.exp (F x), with F (x + 2π) = F x + 2π and F' > 0. This file extends σ to a diffeomorphism of the closed unit disc of ℂ, in the sense of manifolds with boundary. This is what lets data bounded by a parametrized circle, such as a slice disc of a knot, be reparametrized along with the circle.

The extension TauCeti.circleLiftDiffeomorph is a diffeomorphism of the whole plane. It turns the circle of radius r by the circle map with lift

x ↦ x + χ r * (F x - x),

where χ r = smoothTransition (3 r - 1) is 0 for r ≤ 1 / 3 and 1 for r ≥ 2 / 3 (TauCeti.circleLiftDiffeomorph_mul_exp). Since F x - x is 2π-periodic, this is a well defined map on each circle. It interpolates between the identity near the origin and σ on, and outside, the circle of radius 2 / 3. Every interpolating lift has positive derivative (1 - χ r) + χ r * F' x, so the map is a bijection of each circle; it is smooth, and its derivative is invertible everywhere. By the inverse function theorem its inverse is smooth too. It preserves the norm (TauCeti.norm_circleLiftDiffeomorph), so it restricts to a diffeomorphism TauCeti.circleLiftDiscDiffeomorph of the closed unit disc which is σ on the boundary circle (TauCeti.circleLiftDiscDiffeomorph_inclusion).

The same radial interpolation through circle diffeomorphisms is AddCircle.collarDiffeomorphOfLift, on the product ℝ × AddCircle T of a collar coordinate and the circle. Here it is carried out directly on the plane, where it is the identity near the origin and so extends smoothly across the centre of the disc. Both constructions use the interpolating lift lemmas AddCircle.add_mul_sub_add_period, AddCircle.hasDerivAt_add_mul_sub and AddCircle.one_sub_add_mul_pos.

Main definitions

• TauCeti.circleLiftDiffeomorph: the diffeomorphism of ℂ extending the circle map with lift F.
• TauCeti.circleLiftDiscDiffeomorph: its restriction to the closed unit disc.

Main results

• TauCeti.circleLiftDiffeomorph_mul_exp: the value at r * exp (x * I).
• TauCeti.norm_circleLiftDiffeomorph: the diffeomorphism preserves the norm.
• TauCeti.circleLiftDiffeomorph_of_norm_le: it is the identity on the disc of radius 1 / 3.
• TauCeti.circleLiftDiffeomorph_mul_exp_of_le: it is the circle map with lift F on each circle of radius at least 2 / 3.
• TauCeti.norm_circleLiftDiffeomorph_symm, TauCeti.circleLiftDiffeomorph_symm_of_norm_le, TauCeti.circleLiftDiffeomorph_symm_mul_exp_of_le: the same for the inverse.
• TauCeti.circleLiftDiscDiffeomorph_inclusion: on the boundary circle of the closed unit disc the restriction is the circle map with lift F.

References

• M. W. Hirsch, Differential Topology, Graduate Texts in Mathematics 33, Springer, 1976, Chapter 8, §1, for extending a diffeomorphism isotopic to the identity over a collar by a radial cutoff of the isotopy.

The plane map

Smoothness

Bijectivity

The derivative

The diffeomorphisms

noncomputable def TauCeti.circleLiftDiffeomorph {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) : Diffeomorph (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) ℂ ℂ ↑⊤

The diffeomorphism of ℂ extending the circle map with lift F: it turns the circle of radius r by the circle map with lift x ↦ x + smoothTransition (3 r - 1) * (F x - x), so it is the identity near the origin and the circle map with lift F on and outside the circle of radius 2 / 3.

theorem TauCeti.circleLiftDiffeomorph_mul_exp {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) {r : ℝ} (hr : 0 ≤ r) (x : ℝ) : (circleLiftDiffeomorph hper hF hpos) (↑r * Complex.exp (↑x * Complex.I)) = ↑r * Complex.exp (↑(x + (3 * r - 1).smoothTransition * (F x - x)) * Complex.I)

The diffeomorphism turns the circle of radius r by the circle map with lift x ↦ x + smoothTransition (3 r - 1) * (F x - x).

theorem TauCeti.circleLiftDiffeomorph_mul_exp_of_le {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) {r : ℝ} (hr : 2 / 3 ≤ r) (x : ℝ) : (circleLiftDiffeomorph hper hF hpos) (↑r * Complex.exp (↑x * Complex.I)) = ↑r * Complex.exp (↑(F x) * Complex.I)

On and outside the circle of radius 2 / 3 the diffeomorphism is the circle map with lift F on each circle about the origin.

@[simp]

theorem TauCeti.norm_circleLiftDiffeomorph {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) (z : ℂ) : ‖(circleLiftDiffeomorph hper hF hpos) z‖ = ‖z‖

The diffeomorphism preserves the norm.

theorem TauCeti.circleLiftDiffeomorph_of_norm_le {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) {z : ℂ} (hz : ‖z‖ ≤ 1 / 3) : (circleLiftDiffeomorph hper hF hpos) z = z

The diffeomorphism is the identity on the closed disc of radius 1 / 3.

@[simp]

theorem TauCeti.norm_circleLiftDiffeomorph_symm {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) (z : ℂ) : ‖(circleLiftDiffeomorph hper hF hpos).symm z‖ = ‖z‖

The inverse diffeomorphism preserves the norm.

theorem TauCeti.circleLiftDiffeomorph_symm_of_norm_le {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) {z : ℂ} (hz : ‖z‖ ≤ 1 / 3) : (circleLiftDiffeomorph hper hF hpos).symm z = z

The inverse diffeomorphism is the identity on the closed disc of radius 1 / 3.

theorem TauCeti.circleLiftDiffeomorph_symm_mul_exp_of_le {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) {r : ℝ} (hr : 2 / 3 ≤ r) (x : ℝ) : (circleLiftDiffeomorph hper hF hpos).symm (↑r * Complex.exp (↑(F x) * Complex.I)) = ↑r * Complex.exp (↑x * Complex.I)

On and outside the circle of radius 2 / 3 the inverse diffeomorphism undoes the circle map with lift F on each circle about the origin.

noncomputable def TauCeti.circleLiftDiscDiffeomorph {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) : Diffeomorph (modelWithCornersEuclideanHalfSpace 2) (modelWithCornersEuclideanHalfSpace 2) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑⊤

The diffeomorphism of the closed unit disc of ℂ extending the circle map with lift F.

@[simp]

theorem TauCeti.coe_circleLiftDiscDiffeomorph_apply {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) (z : ↑(Metric.closedBall 0 1)) : ↑((circleLiftDiscDiffeomorph hper hF hpos) z) = (circleLiftDiffeomorph hper hF hpos) ↑z

@[simp]

theorem TauCeti.coe_circleLiftDiscDiffeomorph_symm_apply {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) (z : ↑(Metric.closedBall 0 1)) : ↑((circleLiftDiscDiffeomorph hper hF hpos).symm z) = (circleLiftDiffeomorph hper hF hpos).symm ↑z

theorem TauCeti.circleLiftDiscDiffeomorph_inclusion {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + 2 * Real.pi) = F x + 2 * Real.pi) (hF : ContDiff ℝ (↑⊤) F) (hpos : ∀ (x : ℝ), 0 < deriv F x) {σ : Circle → Circle} (hσ : ∀ (x : ℝ), σ (Circle.exp x) = Circle.exp (F x)) (z : Circle) : (circleLiftDiscDiffeomorph hper hF hpos) (Set.inclusion ⋯ z) = Set.inclusion ⋯ (σ z)

On the boundary circle the diffeomorphism of the closed unit disc is the circle map σ with lift F.