OAI/Analysis/Mahler/RescaledHolomorphic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerRescaling.rescale line 11
2. theorem OAI.MahlerRescaling.rescaled_holomorphic_remainder_C2_bound line 16

   Source documentation

   Uniform control of the entire second-order jet of a holomorphic Taylor remainder near the unit sphere, derived from the punctured bound.

   theorem rescaled_holomorphic_remainder_C2_bound {f : E → ℂ} {m : ℕ} {U : Set E}
       (hU : IsOpen U) (hzero : (0 : E) ∈ U) (hf : DifferentiableOn ℂ f U)
       (hf0 : f 0 = 0) (hrem : f =O[𝓝[≠] 0] (fun z : E => ‖z‖^(m+1))) :
       ∃ C > 0, ∃ δ > 0, ∀ ε : ℝ, 0 < ε → ε < δ →
         DifferentiableOn ℂ (rescale f m ε) (ball 0 4) ∧
         ∀ z ∈ closedBall (0 : E) 2,
           ‖rescale f m ε z‖ ≤ C*ε ∧
           ‖fderiv ℂ (rescale f m ε) z‖ ≤ C*ε ∧
           ‖fderiv ℂ (fderiv ℂ (rescale f m ε)) z‖ ≤ C*ε := by
   …

   Mentions: OAI.MahlerRescaling.rescale

3. theorem OAI.MahlerRescaling.rescaled_holomorphic_remainder_uniform_C2 line 52

   Source documentation

   Quantitative uniform bounds tend to zero in all three jet norms.

   theorem rescaled_holomorphic_remainder_uniform_C2 {f : E → ℂ} {m : ℕ} {U : Set E}
       (hU : IsOpen U) (hzero : (0 : E) ∈ U) (hf : DifferentiableOn ℂ f U)
       (hf0 : f 0 = 0) (hrem : f =O[𝓝[≠] 0] (fun z : E => ‖z‖^(m+1))) :
       TendstoUniformlyOn (fun ε : ℝ => rescale f m ε) (fun _ => 0) (𝓝[>] 0) (closedBall 0 2) ∧
       TendstoUniformlyOn (fun ε : ℝ => fderiv ℂ (rescale f m ε)) (fun _ => 0)
         (𝓝[>] 0) (closedBall 0 2) ∧
       TendstoUniformlyOn (fun ε : ℝ => fderiv ℂ (fderiv ℂ (rescale f m ε))) (fun _ => 0)
         (𝓝[>] 0) (closedBall 0 2) := by
   …

   Mentions: OAI.MahlerRescaling.rescale