English
If certain regularity and boundedness conditions hold, cuspFunction is differentiable at 0.
Русский
Если выполняются условия регулярности и ограниченности, cuspFunction дифференцируема в 0.
LaTeX
$$$DifferentiableAt_{\mathbb{C}}(cuspFunction(h,f),0)$ under suitable hypotheses$$
Lean4
theorem differentiableAt_cuspFunction_zero (hh : 0 < h) (hf : Periodic f h) (h_hol : ∀ᶠ z in I∞, DifferentiableAt ℂ f z)
(h_bd : BoundedAtFilter I∞ f) : DifferentiableAt ℂ (cuspFunction h f) 0 :=
by
obtain ⟨c, t⟩ := (boundedAtFilter_cuspFunction hh h_bd).bound
replace t := (eventually_differentiableAt_cuspFunction_nhds_ne_zero hh hf h_hol).and t
simp only [norm_one, Pi.one_apply, mul_one] at t
obtain ⟨S, hS1, hS2, hS3⟩ := eventually_nhds_iff.mp (eventually_nhdsWithin_iff.mp t)
have h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0}) := fun x hx ↦ (hS1 x hx.1 hx.2).1.differentiableWithinAt
have hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0})) :=
by
use c
simp only [mem_upperBounds, Set.mem_image, Set.mem_diff, forall_exists_index, and_imp]
intro y q hq hq2 hy
simpa only [← hy, norm_one, mul_one] using (hS1 q hq hq2).2
have := differentiableOn_update_limUnder_of_bddAbove (IsOpen.mem_nhds hS2 hS3) h_diff hF_bd
rw [← cuspFunction_zero_eq_limUnder_nhds_ne, update_eq_self] at this
exact this.differentiableAt (IsOpen.mem_nhds hS2 hS3)
