OAI/NumberTheory/EgyptianFractions/DivisorPrefixCounting.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorMoment.sum_le_assigned_divisor_majorant line 9

   Source documentation

   Weighted counting for divisors assigned to integers in a translated interval. The pfx map need not be injective or canonical.

   theorem sum_le_assigned_divisor_majorant
       (N Y : ℕ) (A D : Finset ℕ) (pfx : ℕ → ℕ) (w a : ℕ → ℝ)
       (hA : A ⊆ Finset.Ioc N (N + Y))
       (hmap : ∀ n ∈ A, pfx n ∈ D)
       (hdvd : ∀ n ∈ A, pfx n ∣ n)
       (hweight : ∀ n ∈ A, w n ≤ a (pfx n))
       (ha : ∀ d ∈ D, 0 ≤ a d)
       (hD : ∀ d ∈ D, 0 < d ∧ d ≤ Y) :
       (∑ n ∈ A, w n) ≤ 2 * (Y : ℝ) * ∑ d ∈ D, a d / d := by
   …

   Mentions: OAI.Problem337.D

2. theorem OAI.Problem337.DivisorMoment.sum_le_divisor_majorant line 50

   Source documentation

   A choice-free formulation: every integer only needs some admissible pfx divisor, with a uniform nonnegative majorant indexed by that divisor.

   theorem sum_le_divisor_majorant
       (N Y : ℕ) (A D : Finset ℕ) (w a : ℕ → ℝ)
       (hA : A ⊆ Finset.Ioc N (N + Y))
       (hassign : ∀ n ∈ A, ∃ d ∈ D, d ∣ n ∧ w n ≤ a d)
       (ha : ∀ d ∈ D, 0 ≤ a d)
       (hD : ∀ d ∈ D, 0 < d ∧ d ≤ Y) :
       (∑ n ∈ A, w n) ≤ 2 * (Y : ℝ) * ∑ d ∈ D, a d / d := by
   …

   Mentions: OAI.Problem337.D

3. theorem OAI.Problem337.DivisorMoment.sum_le_divisor_majorant_real_cutoff line 72

   Source documentation

   The short interval may have a real length, as in the uniform divisor moment statement. No rounding loss is introduced.

   theorem sum_le_divisor_majorant_real_cutoff
       (N : ℕ) (Y : ℝ) (A D : Finset ℕ) (w a : ℕ → ℝ) (hY : 0 ≤ Y)
       (hA : A ⊆ Finset.Ioc N (N + ⌊Y⌋₊))
       (hassign : ∀ n ∈ A, ∃ d ∈ D, d ∣ n ∧ w n ≤ a d)
       (ha : ∀ d ∈ D, 0 ≤ a d)
       (hD : ∀ d ∈ D, 0 < d ∧ (d : ℝ) ≤ Y) :
       (∑ n ∈ A, w n) ≤ 2 * Y * ∑ d ∈ D, a d / d := by
   …

   Mentions: OAI.Problem337.D