OAI/NumberTheory/EgyptianFractions/ResidueWideDenominator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.ResidueConstruction.residue_size_budget_wide line 9

   Source documentation

   The wide prime pool fits the same auxiliary-denominator size budget.

   theorem residue_size_budget_wide {S : ℝ} {m a : ℕ}
       (hlog : 1 ≤ Real.log S) (hlarge : 100 * Real.log S ≤ S)
       (hmLower : S - Real.log S ≤ (m : ℝ) * Real.log S)
       (hmUpper : (m : ℝ) * Real.log S ≤ S)
       (ha : (a : ℝ) * Real.log 2 ≤ 100000 * Real.log S + Real.log 2) :
       S < (m : ℝ) * (100 * Real.log S) ∧
         (a : ℝ) * Real.log 2 + (2 * (1000 : ℝ) + 1) * (m : ℝ) *
           (101 * Real.log S) ≤ 204204 * S ∧
         (m : ℝ) * (101 * Real.log S) ≤ 101 * S := by
   …

2. theorem OAI.Problem337.ResidueConstruction.construct_residue_denominator_wide line 26

   Source documentation

   PNT-free factor-window variant of the residue denominator construction.

   theorem construct_residue_denominator_wide {m : ℕ} (p : Fin m → ℕ)
       (q : Fin 1000 → Fin m → Fin 2 → ℕ) (hp : ∀ j, 0 < p j)
       (hq : ∀ i j e, 0 < q i j e) {S : ℝ}
       (hS : 1 ≤ S) (hlog : 1 ≤ Real.log S) (hlarge : 100 * Real.log S ≤ S)
       (hmLower : S - Real.log S ≤ (m : ℝ) * Real.log S)
       (hmUpper : (m : ℝ) * Real.log S ≤ S)
       (hpL : ∀ j, 100 * Real.log S ≤ Real.log (p j : ℝ))
       (hpU : ∀ j, Real.log (p j : ℝ) ≤ 101 * Real.log S)
       (hqU : ∀ i j e, Real.log (q i j e : ℝ) ≤ 101 * Real.log S) :
       ∃ M : ℕ, Real.exp S < (M : ℝ) ∧ (M : ℝ) ≤ Real.exp (204204 * S) ∧
         2 ^ ⌈100000 * Real.log S / Real.log 2⌉₊ ∣ M ∧
         (∀ I : Fin m → Fin 2, subsetEntry p I ∣ M ∧ 1 ≤ subsetEntry p I ∧
   …

   Mentions: OAI.Problem337.ResidueConstruction.subsetEntry