English
If h ≠ 0, f is periodic with period h, z is a differentiability point of f, then cuspFunction is differentiable at qParam(h,z).
Русский
Если h ≠ 0, f периодична с периодом h, z — точка дифференцируемости f, то cuspFunction дифференцируема в qParam(h,z).
LaTeX
$$$h \neq 0 \land \text{Periodic}(f,h) \Rightarrow \text{DifferentiableAt}_{\mathbb{C}}( cuspFunction(h,f), qParam(h,z) )$$$
Lean4
/-- Key technical lemma: the function `cuspFunction h f` is differentiable at the images of
differentiability points of `f` (even if `invQParam` is not differentiable there).
-/
theorem differentiableAt_cuspFunction (hh : h ≠ 0) (hf : Periodic f h) {z : ℂ} (hol_z : DifferentiableAt ℂ f z) :
DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z) :=
by
let q := 𝕢 h z
have qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * π * I / h)) z := by
simpa only [id_eq, mul_one] using (((hasStrictDerivAt_id z).const_mul _).div_const _).cexp
have diff_ne : q * (2 * π * I / h) ≠ 0 := mul_ne_zero (exp_ne_zero _) (div_ne_zero two_pi_I_ne_zero <| mod_cast hh)
let L := (qdiff.localInverse (𝕢 h) _ z) diff_ne
have diff_L : DifferentiableAt ℂ L q := (qdiff.to_localInverse diff_ne).differentiableAt
have hL : 𝕢 h ∘ L =ᶠ[𝓝 q] (id : ℂ → ℂ) := (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_right_inverse
have hF := hL.fun_comp (cuspFunction h f)
have : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L := funext fun z ↦ eq_cuspFunction hh hf (L z)
rw [this] at hF
rw [← EventuallyEq.eq_of_nhds (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_left_inverse] at hol_z
exact (hol_z.comp q diff_L).congr_of_eventuallyEq hF.symm
