OAI/NumberTheory/EgyptianFractions/RationalPhaseSpacing.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.RationalPhaseSpacing.separation_of_rational_approximation line 12

   Source documentation

   A reduced rational approximation with error at most q⁻² separates frequencies whose index difference has absolute value at most q/2. The estimate is uniform over every possible nearest integer.

   theorem separation_of_rational_approximation
       (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (h : ℤ) (hne : h ≠ 0) (hsmall : 2 * |h| ≤ (q : ℤ)) (k : ℤ) :
       1 / (2 * (q : ℝ)) ≤ |α * (h : ℝ) - k| := by
   …

2. theorem OAI.Problem337.RationalPhaseSpacing.fract_separation line 54

   Source documentation

   Fractional parts at two nearby distinct integer indices are separated under the same reduced rational approximation.

   theorem fract_separation
       (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (m n : ℤ) (hne : m ≠ n) (hsmall : 2 * |m - n| ≤ (q : ℤ)) :
       1 / (2 * (q : ℝ)) ≤ |Int.fract (α * m) - Int.fract (α * n)| := by
   …

3. theorem OAI.Problem337.RationalPhaseSpacing.card_fract_interval_le_one line 66

   Source documentation

   The fractional parts of a short block occupy each interval of length 1/(2q) at most once. Half-open endpoints are important at exact spacing.

   theorem card_fract_interval_le_one
       (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (A : Finset ℤ) (hspan : ∀ m ∈ A, ∀ n ∈ A, 2 * |m - n| ≤ (q : ℤ))
       (b : ℝ) :
       (A.filter (fun n : ℤ => b ≤ Int.fract (α * (n : ℝ)) ∧
         Int.fract (α * (n : ℝ)) < b + 1 / (2 * (q : ℝ)))).card ≤ 1 := by
   …

4. def OAI.Problem337.RationalPhaseSpacing.phaseBin line 87

   Source documentation

   A canonical finite bin index for the phase of an integer.

   def phaseBin (q : ℕ) (α : ℝ) (n : ℤ) : ℕ :=
   …

5. theorem OAI.Problem337.RationalPhaseSpacing.phaseBin_lt line 90
6. theorem OAI.Problem337.RationalPhaseSpacing.phaseBin_injOn line 99

   Source documentation

   Bin encoding preserves the multiplicity of indices in every short block: no two indices have the same bin.

   theorem phaseBin_injOn
       (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (A : Finset ℤ) (hspan : ∀ m ∈ A, ∀ n ∈ A, 2 * |m - n| ≤ (q : ℤ)) :
       Set.InjOn (phaseBin q α) A := by
   …

   Mentions: OAI.Problem337.RationalPhaseSpacing.phaseBin

7. def OAI.Problem337.RationalPhaseSpacing.truncatedInv line 130

   Source documentation

   A reciprocal truncated at Y, with its correct value at the singular point. The special value is needed for geometric exponential sums.

   def truncatedInv (Y x : ℝ) : ℝ := if x = 0 then Y else min Y (1 / x)

8. theorem OAI.Problem337.RationalPhaseSpacing.truncatedInv_nonneg line 132
9. theorem OAI.Problem337.RationalPhaseSpacing.truncatedInv_le_cap line 139
10. def OAI.Problem337.RationalPhaseSpacing.binWeight line 146

    Source documentation

    Bin majorant for the one-sided reciprocal distance.

    def binWeight (H : ℕ) (Y : ℝ) (j : ℕ) : ℝ :=
    …

11. theorem OAI.Problem337.RationalPhaseSpacing.binWeight_nonneg line 149
12. theorem OAI.Problem337.RationalPhaseSpacing.truncatedInv_fract_le_binWeight line 156
13. theorem OAI.Problem337.RationalPhaseSpacing.sum_binWeight_le line 174

    Source documentation

    Summing the bin majorants costs one singular term and a harmonic sum.

    theorem sum_binWeight_le (H : ℕ) (hH : 0 < H) (Y : ℝ) :
        (∑ j ∈ Finset.range H, binWeight H Y j) ≤
          Y + (H : ℝ) * (1 + Real.log (H : ℝ)) := by
    …

    Mentions: OAI.Problem337.RationalPhaseSpacing.binWeight

14. theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_fract_le line 202

    Source documentation

    A reduced rational approximation controls the sum of truncated one-sided reciprocal distances on every short block. No cancellation hypothesis is used.

    theorem sum_truncatedInv_fract_le
        (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
        (hcop : IsCoprime a (q : ℤ))
        (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
        (A : Finset ℤ) (hspan : ∀ m ∈ A, ∀ n ∈ A, 2 * |m - n| ≤ (q : ℤ))
        (Y : ℝ) (hY : 0 ≤ Y) :
        (∑ n ∈ A, truncatedInv Y (Int.fract (α * n))) ≤
          Y + (2 * (q : ℝ)) * (1 + Real.log (2 * (q : ℝ))) := by
    …

    Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv

15. def OAI.Problem337.RationalPhaseSpacing.intDistance line 229

    Source documentation

    Distance of a real phase to the nearest integer, expressed without a choice of nearest integer.

    def intDistance (x : ℝ) : ℝ := min (Int.fract x) (1 - Int.fract x)

16. theorem OAI.Problem337.RationalPhaseSpacing.intDistance_eq_abs_sub_round line 231
17. theorem OAI.Problem337.RationalPhaseSpacing.intDistance_nonneg line 234
18. theorem OAI.Problem337.RationalPhaseSpacing.truncatedInv_intDistance_le line 239

    Source documentation

    Two one-sided reciprocal majorants control the nearest-integer one, including integer phases where the truncation must equal Y.

    theorem truncatedInv_intDistance_le {Y : ℝ} (hY : 0 ≤ Y) (x : ℝ) :
        truncatedInv Y (intDistance x) ≤
          truncatedInv Y (Int.fract x) + truncatedInv Y (Int.fract (-x)) := by
    …

    Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

19. theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_intDistance_le line 257

    Source documentation

    The classical truncated reciprocal-distance estimate on one short block, with an explicit constant and correct treatment of integer phases.

    theorem sum_truncatedInv_intDistance_le
        (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
        (hcop : IsCoprime a (q : ℤ))
        (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
        (A : Finset ℤ) (hspan : ∀ m ∈ A, ∀ n ∈ A, 2 * |m - n| ≤ (q : ℤ))
        (Y : ℝ) (hY : 0 ≤ Y) :
        (∑ n ∈ A, truncatedInv Y (intDistance (α * n))) ≤
          2 * Y + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ))) := by
    …

    Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

20. theorem OAI.Problem337.RationalPhaseSpacing.short_interval_span line 279

    Source documentation

    Any interval of floor(q/2)+1 consecutive integers is a short block.

    theorem short_interval_span (q : ℕ) (L : ℤ) :
        ∀ m ∈ Finset.Ico L (L + (q / 2 : ℕ) + 1),
          ∀ n ∈ Finset.Ico L (L + (q / 2 : ℕ) + 1),
            2 * |m - n| ≤ (q : ℤ) := by
    …

21. theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_intDistance_short_interval_le line 294

    Source documentation

    Interval form of the short-block estimate used in Type I/II decompositions.

    theorem sum_truncatedInv_intDistance_short_interval_le
        (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
        (hcop : IsCoprime a (q : ℤ))
        (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
        (L : ℤ) (Y : ℝ) (hY : 0 ≤ Y) :
        (∑ n ∈ Finset.Ico L (L + (q / 2 : ℕ) + 1), truncatedInv Y (intDistance (α * n))) ≤
          2 * Y + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ))) :=
    …

    Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

22. theorem OAI.Problem337.RationalPhaseSpacing.sum_int_Ico_add line 303
23. theorem OAI.Problem337.RationalPhaseSpacing.sum_int_Ico_le_blocks line 320

    Source documentation

    Aggregate an estimate on consecutive blocks, with no periodicity premise.

    theorem sum_int_Ico_le_blocks (f : ℤ → ℝ) (B : ℕ) (hB : 0 < B) (C : ℝ)
        (hblock : ∀ L : ℤ, (∑ n ∈ Finset.Ico L (L + B), f n) ≤ C)
        (L : ℤ) (k : ℕ) :
        (∑ n ∈ Finset.Ico L (L + (k : ℤ) * B), f n) ≤ (k : ℝ) * C := by
    …

24. theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_intDistance_interval_le_blocks line 340

    Source documentation

    Full interval version, with the exact number of short blocks.

    theorem sum_truncatedInv_intDistance_interval_le_blocks
        (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
        (hcop : IsCoprime a (q : ℤ))
        (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
        (L : ℤ) (N : ℕ) (Y : ℝ) (hY : 0 ≤ Y) :
        (∑ n ∈ Finset.Ico L (L + N), truncatedInv Y (intDistance (α * n))) ≤
          ((N / (q / 2 + 1) + 1 : ℕ) : ℝ) *
            (2 * Y + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ)))) := by
    …

    Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance

25. theorem OAI.Problem337.RationalPhaseSpacing.sum_truncatedInv_intDistance_interval_le line 368

    Source documentation

    Standard convenient full-interval form of the rational approximation reciprocal-distance estimate. It applies equally to negative interval origins.

    theorem sum_truncatedInv_intDistance_interval_le
        (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
        (hcop : IsCoprime a (q : ℤ))
        (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
        (L : ℤ) (N : ℕ) (Y : ℝ) (hY : 0 ≤ Y) :
        (∑ n ∈ Finset.Ico L (L + N), truncatedInv Y (intDistance (α * n))) ≤
          (2 * (N : ℝ) / q + 1) *
            (2 * Y + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ)))) := by
    …

    Mentions: OAI.Problem337.RationalPhaseSpacing.truncatedInv, OAI.Problem337.RationalPhaseSpacing.intDistance