RescalingEstimates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.MahlerRescaling.fderiv_bound_of_ball_bound line 16

Source documentation

A centered Schwarz bound with a uniform bound on values.

lemma fderiv_bound_of_ball_bound {f : E → F} {x : E} {R r C : ℝ}
    (hr : 0 < r) (hx : ‖x‖ + r ≤ R)
    (hf : DifferentiableOn ℂ f (ball 0 R))
    (hbound : ∀ z ∈ ball (0 : E) R, ‖f z‖ ≤ C) :
    ‖fderiv ℂ f x‖ ≤ 2*C/r := by
…

theorem OAI.MahlerRescaling.two_derivative_bounds line 36

Source documentation

Two nested Schwarz estimates give uniform first and second derivative bounds on a fixed neighborhood of the unit sphere.

theorem two_derivative_bounds {f : E → F} {C : ℝ}
    (hf : DifferentiableOn ℂ f (ball 0 4))
    (hf' : DifferentiableOn ℂ (fderiv ℂ f) (ball 0 4))
    (hbound : ∀ z ∈ ball (0 : E) 4, ‖f z‖ ≤ C) :
    ∀ z ∈ closedBall (0 : E) 2,
      ‖f z‖ ≤ C ∧ ‖fderiv ℂ f z‖ ≤ 2*C ∧
        ‖fderiv ℂ (fderiv ℂ f) z‖ ≤ 4*C := by
…

theorem OAI.MahlerRescaling.rescaled_remainder_bound line 63

Source documentation

The punctured Taylor estimate yields a uniform O(epsilon) bound after rescaling on any prescribed bounded ball. This includes the center.

theorem rescaled_remainder_bound {f : E → F} {m : ℕ} (hf0 : f 0 = 0)
    (hf : f =O[𝓝[≠] 0] (fun z : E => ‖z‖^(m+1))) {B : ℝ} (hB : 0 < B) :
    ∃ C > 0, ∃ δ > 0, ∀ ε : ℝ, 0 < ε → ε < δ →
      ∀ z : E, ‖z‖ ≤ B → ‖(ε^m)⁻¹ • f (ε • z)‖ ≤ C*ε := by
…