OAI/NumberTheory/EgyptianFractions/DiscreteSecondDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.nat_separated_near_integer_card line 12

   Source documentation

   Natural-indexed strict-neighborhood version of the separated sample bound.

   theorem nat_separated_near_integer_card (d : ℕ → ℝ) (N : ℕ)
       (lam β L U : ℝ) (hlam : 0 < lam) (hβ : 0 ≤ β) (hLU : L ≤ U)
       (hsep : ∀ i < N, ∀ j < N, i ≤ j → lam * ((j : ℝ) - i) ≤ d j - d i)
       (hrange : ∀ i < N, L ≤ d i ∧ d i ≤ U) :
       ((nearIntegerIndices d N β).card : ℝ) ≤
         (U - L + 2 * β + 1) * (2 * β / lam + 1) := by
   …

   Mentions: OAI.Problem337.nearIntegerIndices

2. theorem OAI.Problem337.ExponentialSum.first_derivative_Ico_bound line 47

   Source documentation

   A strip cancellation bound needing increment information only for the indices being summed; the final endpoint costs at most one.

   theorem first_derivative_Ico_bound (f : ℕ → ℝ) (a b : ℕ) (β : ℝ) (q : ℤ)
       (hab : a ≤ b) (hβ : 0 < β)
       (hlo : ∀ j ∈ Finset.Ico a b, (q : ℝ) + β ≤ f (j + 1) - f j)
       (hhi : ∀ j ∈ Finset.Ico a b, f (j + 1) - f j ≤ (q : ℝ) + 1 - β)
       (hmono : MonotoneOn (fun j => f (j + 1) - f j) (Set.Iio b)) :
       ‖∑ j ∈ Finset.Ico a b, phase (f j)‖ ≤ 2 / β + 1 := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase

3. theorem OAI.Problem337.ExponentialSum.discrete_second_derivative_partition_bound line 86

   Source documentation

   A fully discrete second-derivative estimate from monotone separated phase increments. The only analytic input is the proved first-derivative test.

   theorem discrete_second_derivative_partition_bound (f : ℕ → ℝ) (N : ℕ)
       (lam β L U : ℝ) (hlam : 0 < lam) (hβ : 0 < β) (hLU : L ≤ U)
       (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 ≤ U) :
       ‖∑ j ∈ Finset.range N, phase (f j)‖ ≤
         (U - L + 2 * β + 1) * (2 * β / lam + 1) + (U - L + 2) * (2 / β + 1) := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase

4. theorem OAI.Problem337.ExponentialSum.discrete_second_derivative_sqrt_bound line 107

   Source documentation

   The square-root form used in the reciprocal-phase differencing argument.

   theorem discrete_second_derivative_sqrt_bound (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