OAI/NumberTheory/EgyptianFractions/ExponentialFirstDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.exponential_first_derivative_bound line 12

   Source documentation

   A discrete first-derivative estimate, with an explicit absolute constant.

   theorem exponential_first_derivative_bound (f d : ℕ → ℝ) (n : ℕ) (β : ℝ)
       (hβ : 0 < β) (hstep : ∀ j ≤ n, f (j + 1) = f j + d j)
       (hbounds : ∀ j ≤ n, β ≤ d j ∧ d j ≤ 1 - β)
       (hmono : (∀ j < n, d j ≤ d (j + 1)) ∨ (∀ j < n, d (j + 1) ≤ d j)) :
       ‖∑ j ∈ Finset.range (n + 1), unitPhase (Real.pi * f j)‖ ≤ 1 / β := by
   …

2. lemma OAI.Problem337.unitPhase_int_pi line 56
3. lemma OAI.Problem337.unitPhase_add_int_pi line 62
4. lemma OAI.Problem337.unitPhase_pi_sub_int line 66
5. theorem OAI.Problem337.exponential_first_derivative_int_cell line 74

   Source documentation

   The first-derivative estimate on any fixed integer cell of increments.

   theorem exponential_first_derivative_int_cell (f d : ℕ → ℝ) (n : ℕ) (m : ℤ) (β : ℝ)
       (hβ : 0 < β) (hstep : ∀ j ≤ n, f (j + 1) = f j + d j)
       (hbounds : ∀ j ≤ n, (m : ℝ) + β ≤ d j ∧ d j ≤ (m : ℝ) + 1 - β)
       (hmono : (∀ j < n, d j ≤ d (j + 1)) ∨ (∀ j < n, d (j + 1) ≤ d j)) :
       ‖∑ j ∈ Finset.range (n + 1), unitPhase (Real.pi * f j)‖ ≤ 1 / β := by
   …

6. theorem OAI.Problem337.exponential_first_derivative_Ico line 107

   Source documentation

   Interval form for splitting an exponential sum into monotone integer cells.

   theorem exponential_first_derivative_Ico (f d : ℕ → ℝ) (a b : ℕ) (m : ℤ) (β : ℝ)
       (hab : a < b) (hβ : 0 < β)
       (hstep : ∀ j ∈ Finset.Ico a b, f (j + 1) = f j + d j)
       (hbounds : ∀ j ∈ Finset.Ico a b,
         (m : ℝ) + β ≤ d j ∧ d j ≤ (m : ℝ) + 1 - β)
       (hmono : MonotoneOn d (Set.Ico a b) ∨ AntitoneOn d (Set.Ico a b)) :
       ‖∑ j ∈ Finset.Ico a b, unitPhase (Real.pi * f j)‖ ≤ 1 / β := by
   …