OAI/NumberTheory/EgyptianFractions/SecondDerivativeTest.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.ExponentialSum.discrete_second_derivative_sqrt_bound_local line 11

   Source documentation

   The discrete test needs monotonicity only at the sampled increments.

   theorem discrete_second_derivative_sqrt_bound_local (f : ℕ → ℝ) (N : ℕ)
       (lam A L : ℝ) (hlam : 0 < lam) (hlam1 : lam ≤ 1) (hA : 0 ≤ A)
       (hmono : MonotoneOn (fun j => f (j + 1) - f j) (Set.Iio N))
       (hsep : ∀ i < N, ∀ j < N, i ≤ j →
         lam * ((j : ℝ) - i) ≤ (f (j + 1) - f j) - (f (i + 1) - f i))
       (hrange : ∀ j < N, L ≤ f (j + 1) - f j ∧
         f (j + 1) - f j ≤ L + A * lam * N) :
       ‖∑ j ∈ Finset.range N, phase (f j)‖ ≤
         6 * A * N * Real.sqrt lam + 6 / Real.sqrt lam + 9 := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase

2. theorem OAI.Problem337.ExponentialSum.translated_sampled_increment_bounds line 45

   Source documentation

   Sampled differences on a translated real interval. The closed support ends at the last needed phase value, not one integer beyond it.

   theorem translated_sampled_increment_bounds (f f' f'' : ℝ → ℝ)
       (x : ℝ) (N i j : ℕ) (L U : ℝ) (_hi : i < N) (hj : j < N) (hij : i ≤ j)
       (hf : ∀ y ∈ Set.Icc x (x + N), HasDerivAt f (f' y) y)
       (hf' : ∀ y ∈ Set.Icc x (x + N), HasDerivAt f' (f'' y) y)
       (hbound : ∀ y ∈ Set.Icc x (x + N), L ≤ f'' y ∧ f'' y ≤ U) :
       L * ((j : ℝ) - i) ≤
           (f (((j + 1 : ℕ) : ℝ) + x) - f ((j : ℝ) + x)) -
           (f (((i + 1 : ℕ) : ℝ) + x) - f ((i : ℝ) + x)) ∧
         (f (((j + 1 : ℕ) : ℝ) + x) - f ((j : ℝ) + x)) -
           (f (((i + 1 : ℕ) : ℝ) + x) - f ((i : ℝ) + x)) ≤ U * ((j : ℝ) - i) := by
   …

3. theorem OAI.Problem337.ExponentialSum.second_derivative_sqrt_bound_positive line 70

   Source documentation

   The second-derivative test for a positive second derivative on precisely the closed interval supporting the finite sum.

   theorem second_derivative_sqrt_bound_positive (f f' f'' : ℝ → ℝ)
       (x : ℝ) (N : ℕ) (lam A : ℝ)
       (hlam : 0 < lam) (hlam1 : lam ≤ 1) (hA : 0 ≤ A)
       (hf : ∀ y ∈ Set.Icc x (x + N), HasDerivAt f (f' y) y)
       (hf' : ∀ y ∈ Set.Icc x (x + N), HasDerivAt f' (f'' y) y)
       (hbound : ∀ y ∈ Set.Icc x (x + N), lam ≤ f'' y ∧ f'' y ≤ A * lam) :
       ‖∑ j ∈ Finset.range N, phase (f ((j : ℝ) + x))‖ ≤
         6 * A * N * Real.sqrt lam + 6 / Real.sqrt lam + 9 := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase

4. theorem OAI.Problem337.ExponentialSum.second_derivative_sqrt_bound line 111

   Source documentation

   The usual absolute second-derivative test. Darboux gives a uniform sign; negative phases are handled by complex conjugation.

   theorem second_derivative_sqrt_bound (f f' f'' : ℝ → ℝ)
       (x : ℝ) (N : ℕ) (lam A : ℝ)
       (hlam : 0 < lam) (hlam1 : lam ≤ 1) (hA : 0 ≤ A)
       (hf : ∀ y ∈ Set.Icc x (x + N), HasDerivAt f (f' y) y)
       (hf' : ∀ y ∈ Set.Icc x (x + N), HasDerivAt f' (f'' y) y)
       (hbound : ∀ y ∈ Set.Icc x (x + N), lam ≤ |f'' y| ∧ |f'' y| ≤ A * lam) :
       ‖∑ j ∈ Finset.range N, phase (f ((j : ℝ) + x))‖ ≤
         6 * A * N * Real.sqrt lam + 6 / Real.sqrt lam + 9 := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase

5. theorem OAI.Problem337.ExponentialSum.second_derivative_sqrt_bound_Ico line 134

   Source documentation

   Natural interval form, requiring derivative bounds only on its closure.

   theorem second_derivative_sqrt_bound_Ico (f f' f'' : ℝ → ℝ)
       (a b : ℕ) (lam A : ℝ) (hab : a ≤ b)
       (hlam : 0 < lam) (hlam1 : lam ≤ 1) (hA : 0 ≤ A)
       (hf : ∀ y ∈ Set.Icc (a : ℝ) (b : ℝ), HasDerivAt f (f' y) y)
       (hf' : ∀ y ∈ Set.Icc (a : ℝ) (b : ℝ), HasDerivAt f' (f'' y) y)
       (hbound : ∀ y ∈ Set.Icc (a : ℝ) (b : ℝ), lam ≤ |f'' y| ∧ |f'' y| ≤ A * lam) :
       ‖∑ j ∈ Finset.Ico a b, phase (f j)‖ ≤
         6 * A * (b - a : ℕ) * Real.sqrt lam + 6 / Real.sqrt lam + 9 := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase

6. theorem OAI.Problem337.ExponentialSum.second_derivative_test line 152

   Source documentation

   A uniform second-derivative estimate for every positive scale, without a smallness hypothesis on that scale or an additive endpoint error.

   theorem second_derivative_test (f f' f'' : ℝ → ℝ)
       (x : ℝ) (N : ℕ) (lam A : ℝ) (hlam : 0 < lam) (hA : 0 ≤ A)
       (hf : ∀ y ∈ Set.Icc x (x + N), HasDerivAt f (f' y) y)
       (hf' : ∀ y ∈ Set.Icc x (x + N), HasDerivAt f' (f'' y) y)
       (hbound : ∀ y ∈ Set.Icc x (x + N), lam ≤ |f'' y| ∧ |f'' y| ≤ A * lam) :
       ‖∑ j ∈ Finset.range N, phase (f ((j : ℝ) + x))‖ ≤
         (6 * A + 15) * ((N : ℝ) * Real.sqrt lam + 1 / Real.sqrt lam) := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase

7. theorem OAI.Problem337.ExponentialSum.second_derivative_test_Ico line 184

   Source documentation

   Interval version of the uniform second-derivative test.

   theorem second_derivative_test_Ico (f f' f'' : ℝ → ℝ)
       (a b : ℕ) (lam A : ℝ) (hab : a ≤ b) (hlam : 0 < lam) (hA : 0 ≤ A)
       (hf : ∀ y ∈ Set.Icc (a : ℝ) (b : ℝ), HasDerivAt f (f' y) y)
       (hf' : ∀ y ∈ Set.Icc (a : ℝ) (b : ℝ), HasDerivAt f' (f'' y) y)
       (hbound : ∀ y ∈ Set.Icc (a : ℝ) (b : ℝ), lam ≤ |f'' y| ∧ |f'' y| ≤ A * lam) :
       ‖∑ j ∈ Finset.Ico a b, phase (f j)‖ ≤
         (6 * A + 15) * (((b - a : ℕ) : ℝ) * Real.sqrt lam + 1 / Real.sqrt lam) := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase