Source indexedlemma · leanprover/lean4:v4.32.0

HasDerivAt.of_hasDerivAt_ofReal_comp

PrimeNumberTheoremAnd.Auxiliary · PrimeNumberTheoremAnd/Auxiliary.lean:48 to 57

Mathematical statement

Exact Lean statement

lemma HasDerivAt.of_hasDerivAt_ofReal_comp {z : ℝ} {f : ℝ → ℝ} {u : ℂ}
    (hf : HasDerivAt (fun y ↦ (f y : ℂ)) u z) :
    ∃ u' : ℝ, u = u' ∧ HasDerivAt f u' z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma HasDerivAt.of_hasDerivAt_ofReal_comp {z : ℝ} {f : ℝ → ℝ} {u : ℂ}    (hf : HasDerivAt (fun y ↦ (f y : ℂ)) u z) :    ∃ u' : ℝ, u = u' ∧ HasDerivAt f u' z := by  lift u to ℝ  · have H := (imCLM.hasFDerivAt.comp z hf.hasFDerivAt).hasDerivAt.deriv    simp only [Function.comp_def, imCLM_apply, ofReal_im, deriv_const] at H    rwa [eq_comm, comp_apply, imCLM_apply, toSpanSingleton_apply_one] at H  refine ⟨u, rfl, ?_⟩  convert! (reCLM.hasFDerivAt.comp z hf.hasFDerivAt).hasDerivAt  rw [comp_apply, toSpanSingleton_apply_one, reCLM_apply, ofReal_re]