OAI/Analysis/Mahler/UniformJet.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerRescaling.uniform_of_linear_error line 9
2. lemma OAI.MahlerRescaling.second_fderiv_sub_of_open line 31

   Source documentation

   Differentiating the actual first derivative on an open set preserves subtraction through order two; holomorphicity supplies the required smoothness.

   lemma second_fderiv_sub_of_open {f g : E → ℂ} {U : Set E} {x : E}
       (hU : IsOpen U) (hx : x ∈ U)
       (hf : DifferentiableOn ℂ f U) (hg : DifferentiableOn ℂ g U) :
       fderiv ℂ (fderiv ℂ (fun y => f y-g y)) x =
         fderiv ℂ (fderiv ℂ f) x - fderiv ℂ (fderiv ℂ g) x := by
   …