eventually_differentiableAt_cuspFunction_nhds_ne_zero

English

If h > 0 and f is periodic with period h and f is differentiable for a large family of points, then cuspFunction is differentiable at nearby qParam values.

Русский

Если h > 0, f периодична с периодом h и дифференцируема на большом множестве точек, cuspFunction дифференцируема в ближайших qParam.

LaTeX

$$∀ᶠ z ∈ I∞, DifferentiableAt_ℂ(f,z) → ∀ᶠ q ∈ 𝓝[≠]0, DifferentiableAt_ℂ((cuspFunction h f), q)$$

Lean4

theorem eventually_differentiableAt_cuspFunction_nhds_ne_zero (hh : 0 < h) (hf : Periodic f h)
    (h_hol : ∀ᶠ z in I∞, DifferentiableAt ℂ f z) : ∀ᶠ q in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) q :=
  by
  refine ((invQParam_tendsto hh).eventually h_hol).mp ?_
  refine eventually_nhdsWithin_of_forall (fun q hq h_diff ↦ ?_)
  rw [← qParam_right_inv hh.ne' hq]
  exact differentiableAt_cuspFunction hh.ne' hf h_diff

Похожие утверждения