Periodic lifts on the circle: derivative and smoothness in the translation atlas

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #195.

A function f : ℝ → ℝ of period T descends to hf.lift : AddCircle T → ℝ (Function.Periodic.lift). In the translation atlas of AddCircleTranslation.lean every chart inverse is the quotient map, so the lift read in any chart is f: its manifold derivative is f' and it is as smooth as f.

• Function.Periodic.deriv_periodic — the derivative of a periodic function is periodic;
• Function.Periodic.continuous_lift;
• ★ Function.Periodic.hasMFDerivAt_lift — the manifold derivative of the lift is f', read back on the circle through the lift of f'; mfderiv_lift;
• ★ Function.Periodic.contMDiff_lift — the lift is C^n when f is.

References: Instances/AddCircleTranslation.lean (translationChart, chartAt_eq, coe_translationChart); Mathlib/Algebra/Ring/Periodic.lean (Function.Periodic.lift).

theorem Function.Periodic.deriv_periodic {f : ℝ → ℝ} {T : ℝ} (hf : Periodic f T) : Periodic (deriv f) T

The derivative of a periodic function is periodic.

theorem Function.Periodic.continuous_lift {f : ℝ → ℝ} {T : ℝ} (hf : Periodic f T) (hc : Continuous f) : Continuous hf.lift

The lift is continuous when f is: the quotient map is a quotient map.

theorem Function.Periodic.lift_comp_chart_symm {f : ℝ → ℝ} {T : ℝ} [Fact (0 < T)] (hf : Periodic f T) (x : AddCircle T) (y : ℝ) : hf.lift (↑(chartAt ℝ x).symm y) = f y

Read through any translation chart, the lift is f.

theorem Function.Periodic.deriv_periodic_lift_eq {f : ℝ → ℝ} {T : ℝ} [Fact (0 < T)] (hf : Periodic f T) (x : AddCircle T) : ⋯.lift x = deriv f (↑(chartAt ℝ x) x)

The lift of f' at x is f' at the chart coordinate of x.

theorem Function.Periodic.hasMFDerivAt_lift {f : ℝ → ℝ} {T : ℝ} [Fact (0 < T)] (hf : Periodic f T) (hd : Differentiable ℝ f) (x : AddCircle T) : HasMFDerivAt% hf.lift x (ContinuousLinearMap.smulRight 1 (⋯.lift x))

★ The manifold derivative of the lift is f', for the translation atlas.

theorem Function.Periodic.mfderiv_lift {f : ℝ → ℝ} {T : ℝ} [Fact (0 < T)] (hf : Periodic f T) (hd : Differentiable ℝ f) (x : AddCircle T) : mfderiv% hf.lift x = ContinuousLinearMap.smulRight 1 (⋯.lift x)

theorem Function.Periodic.contMDiff_lift {f : ℝ → ℝ} {T : ℝ} [Fact (0 < T)] (hf : Periodic f T) {n : WithTop ℕ∞} (hc : ContDiff ℝ n f) : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n hf.lift

★ The lift is C^n when f is, for the translation atlas.