SecondDifference.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.second_difference_eq_deriv line 10

Source documentation

A second finite difference is a second derivative value times the squared step. Only pointwise derivative data on the relevant closed interval is used.

theorem second_difference_eq_deriv (f f' f'' : ℝ → ℝ) (x h : ℝ) (hh : 0 < h)
    (hf : ∀ y ∈ Icc x (x + 2 * h), HasDerivAt f (f' y) y)
    (hf' : ∀ y ∈ Icc x (x + 2 * h), HasDerivAt f' (f'' y) y) :
    ∃ c ∈ Ioo x (x + 2 * h),
      f (x + 2 * h) - 2 * f (x + h) + f x = h ^ 2 * f'' c := by
…

theorem OAI.Problem337.second_difference_bounds line 48

Source documentation

Bounds for the second derivative give bounds for each second difference.

theorem second_difference_bounds (f f' f'' : ℝ → ℝ) (x h L U : ℝ) (hh : 0 < h)
    (hf : ∀ y ∈ Icc x (x + 2 * h), HasDerivAt f (f' y) y)
    (hf' : ∀ y ∈ Icc x (x + 2 * h), HasDerivAt f' (f'' y) y)
    (hbound : ∀ y ∈ Icc x (x + 2 * h), L ≤ f'' y ∧ f'' y ≤ U) :
    h ^ 2 * L ≤ f (x + 2 * h) - 2 * f (x + h) + f x ∧
      f (x + 2 * h) - 2 * f (x + h) + f x ≤ h ^ 2 * U := by
…

theorem OAI.Problem337.discrete_increment_bounds line 61

Source documentation

Telescoping a two-sided bound for adjacent increments.

theorem discrete_increment_bounds (d : ℕ → ℝ) (a b : ℕ) (L U : ℝ)
    (hab : a ≤ b)
    (hstep : ∀ j ∈ Finset.Ico a b, L ≤ d (j + 1) - d j ∧ d (j + 1) - d j ≤ U) :
    L * ((b : ℝ) - a) ≤ d b - d a ∧ d b - d a ≤ U * ((b : ℝ) - a) := by
…

theorem OAI.Problem337.sampled_increment_bounds line 79

Source documentation

Continuous second-derivative bounds imply the separation hypotheses for sampled first differences used by the discrete second-derivative test.

theorem sampled_increment_bounds (f f' f'' : ℝ → ℝ) (a b : ℕ) (L U : ℝ)
    (hab : a ≤ b)
    (hf : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), HasDerivAt f (f' y) y)
    (hf' : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), HasDerivAt f' (f'' y) y)
    (hbound : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), L ≤ f'' y ∧ f'' y ≤ U) :
    L * ((b : ℝ) - a) ≤
        (f ((b : ℝ) + 1) - f b) - (f ((a : ℝ) + 1) - f a) ∧
      (f ((b : ℝ) + 1) - f b) - (f ((a : ℝ) + 1) - f a) ≤ U * ((b : ℝ) - a) := by
…

theorem OAI.Problem337.second_derivative_signed_bounds line 105

Source documentation

Darboux's theorem makes the sign of a nonvanishing second derivative constant. Absolute derivative bounds therefore give one uniform signed strip.

theorem second_derivative_signed_bounds (f' f'' : ℝ → ℝ) (s : Set ℝ)
    (hs : Convex ℝ s) (L U : ℝ) (hL : 0 < L)
    (hf' : ∀ x ∈ s, HasDerivAt f' (f'' x) x)
    (hbound : ∀ x ∈ s, L ≤ |f'' x| ∧ |f'' x| ≤ U) :
    (∀ x ∈ s, L ≤ f'' x ∧ f'' x ≤ U) ∨
      (∀ x ∈ s, -U ≤ f'' x ∧ f'' x ≤ -L) := by
…

theorem OAI.Problem337.sampled_increment_abs_bounds line 129

Source documentation

Positive lower absolute second-derivative bounds give separation of all sampled first differences, whether the second derivative is positive or negative.

theorem sampled_increment_abs_bounds (f f' f'' : ℝ → ℝ) (a b : ℕ) (L U : ℝ)
    (hab : a ≤ b) (hL : 0 < L)
    (hf : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), HasDerivAt f (f' y) y)
    (hf' : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), HasDerivAt f' (f'' y) y)
    (hbound : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), L ≤ |f'' y| ∧ |f'' y| ≤ U) :
    L * ((b : ℝ) - a) ≤
        |(f ((b : ℝ) + 1) - f b) - (f ((a : ℝ) + 1) - f a)| ∧
      |(f ((b : ℝ) + 1) - f b) - (f ((a : ℝ) + 1) - f a)| ≤
        U * ((b : ℝ) - a) := by
…

theorem OAI.Problem337.sampled_increment_strictMono_or_strictAnti line 152

Source documentation

Sampled first differences are monotone in one direction under a positive absolute lower bound for the second derivative.

theorem sampled_increment_strictMono_or_strictAnti (f f' f'' : ℝ → ℝ)
    (a b : ℕ) (L U : ℝ) (hL : 0 < L)
    (hf : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), HasDerivAt f (f' y) y)
    (hf' : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), HasDerivAt f' (f'' y) y)
    (hbound : ∀ y ∈ Icc (a : ℝ) ((b : ℝ) + 1), L ≤ |f'' y| ∧ |f'' y| ≤ U) :
    StrictMonoOn (fun n : ℕ => f ((n : ℝ) + 1) - f n) (Icc a b) ∨
      StrictAntiOn (fun n : ℕ => f ((n : ℝ) + 1) - f n) (Icc a b) := by
…