OAI/NumberTheory/EgyptianFractions/ReciprocalTerminalSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.reciprocal_terminal_sqrt_budget line 13

   Source documentation

   Absorb the square-root expression in the second derivative test.

   theorem reciprocal_terminal_sqrt_budget {U a lam T : ℝ} (hU : 1 ≤ U)
       (ha : 0 < a) (hT : T ≤ 3 * U)
       (hlower : a * U ^ (-(3 : ℝ) / 2) ≤ lam)
       (hupper : lam ≤ a * U ^ (-(2 : ℝ) / 5)) :
       T * Real.sqrt lam + 1 / Real.sqrt lam ≤
         3 * (a ^ ((1 : ℝ) / 2) + a ^ (-(1 : ℝ) / 2) + 1) * U ^ ((4 : ℝ) / 5) := by
   …

2. theorem OAI.Problem337.reciprocal_terminal_range_bound line 31

   Source documentation

   Once a fixed reciprocal derivative order has been chosen, every short forward difference satisfies a uniform terminal cancellation estimate.

   theorem reciprocal_terminal_range_bound (k : ℕ) (hk : 4 ≤ k) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ (U Z x : ℝ) (N : ℕ) (hs : List ℝ),
         2 ≤ U → hs.length + 2 = k →
         (∀ h ∈ hs, 1 ≤ h ∧ h ≤ U ^ (1 / (10 * (k : ℝ)))) →
         U ^ (-(3 : ℝ) / 2) ≤ |Z| * U ^ (-((k : ℝ) + 1)) →
         |Z| * U ^ (-((k : ℝ) + 1)) ≤ U ^ (-(1 : ℝ) / 2) →
         U ≤ x → x + N + hs.sum ≤ 3 * U → (N : ℝ) ≤ 3 * U →
         ‖∑ j ∈ Finset.range N,
           ExponentialSum.phase (forwardDifference hs (fun y => Z / y) ((j : ℝ) + x))‖ ≤
           C * U ^ ((4 : ℝ) / 5) := by
   …

   Mentions: OAI.Problem337.ExponentialSum.phase, OAI.Problem337.forwardDifference

3. theorem OAI.Problem337.reciprocal_terminal_interval_bound line 91

   Source documentation

   Integer interval terminal estimate, in the exact form used by iterated correlations. The endpoint extension is absorbed by the enlarged interval.

   theorem reciprocal_terminal_interval_bound (k : ℕ) (hk : 4 ≤ k) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ (U Z : ℝ) (L R : ℤ) (hs : List ℤ),
         2 ≤ U → hs.length = k - 2 →
         (∀ h ∈ hs, 0 < h ∧ h < (Nat.floor (U ^ (1 / (10 * (k : ℝ)))) : ℤ)) →
         U ^ (-(3 : ℝ) / 2) ≤ |Z| * U ^ (-((k : ℝ) + 1)) →
         |Z| * U ^ (-((k : ℝ) + 1)) ≤ U ^ (-(1 : ℝ) / 2) →
         U ≤ (L : ℝ) → (R : ℝ) ≤ 2 * U →
         ‖∑ n ∈ Finset.Icc L (R - hs.sum),
           differencingPhase (forwardDifference (hs.map (fun h : ℤ => (h : ℝ)))
             (fun y => Z / y) n)‖ ≤ C * U ^ ((4 : ℝ) / 5) := by
   …

   Mentions: OAI.Problem337.differencingPhase, OAI.Problem337.forwardDifference

4. theorem OAI.Problem337.reciprocal_terminal_bound_eventually line 146

   Source documentation

   Eventual interface for finite-order uniformization of reciprocal phases.

   theorem reciprocal_terminal_bound_eventually (k : ℕ) (hk : 4 ≤ k) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ᶠ U : ℝ in Filter.atTop, ∀ Z : ℝ,
         U ^ (-(3 : ℝ) / 2) ≤ |Z| * U ^ (-((k : ℝ) + 1)) →
         |Z| * U ^ (-((k : ℝ) + 1)) ≤ U ^ (-(1 : ℝ) / 2) →
         ∀ L R : ℤ, U ≤ (L : ℝ) → (R : ℝ) ≤ 2 * U →
         ∀ hs : List ℤ, hs.length = k - 2 →
         (∀ h ∈ hs, 0 < h ∧ h < (Nat.floor (U ^ (1 / (10 * (k : ℝ)))) : ℤ)) →
         ‖∑ n ∈ Finset.Icc L (R - hs.sum),
           differencingPhase (forwardDifference (hs.map (fun h : ℤ => (h : ℝ)))
             (fun y => Z / y) n)‖ ≤ C * U ^ ((4 : ℝ) / 5) := by
   …

   Mentions: OAI.Problem337.differencingPhase, OAI.Problem337.forwardDifference