Segment Quotient

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.abs_div_le_of_deriv_bound {g : ℝ → ℝ} {x M : ℝ} (hg0 : g 0 = 0) (hd : ∀ s ∈ Set.uIcc 0 x, DifferentiableAt ℝ g s) (hM : ∀ s ∈ Set.uIcc 0 x, |deriv g s| ≤ M) (hx : x ≠ 0) : |g x / x| ≤ M

If g is differentiable on the interval between 0 and x with |deriv g| ≤ M there, then |g x / x| ≤ M whenever x ≠ 0.

theorem CIV.abs_le_mul_of_deriv_bound {g : ℝ → ℝ} {x M : ℝ} (hg0 : g 0 = 0) (hd : ∀ s ∈ Set.uIcc 0 x, DifferentiableAt ℝ g s) (hM : ∀ s ∈ Set.uIcc 0 x, |deriv g s| ≤ M) : |g x| ≤ M * |x|

If g is differentiable on the interval between 0 and x with |deriv g| ≤ M there, then |g x| ≤ M * |x|.