OAI/NumberTheory/EgyptianFractions/ResidueDenominator.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.ResidueConstruction.exists_binary_factor line 10

   Source documentation

   A binary factor can cover any positive cutoff at a logarithmic cost of at most log 2.

   theorem exists_binary_factor {x : ℝ} (hx : 1 ≤ x) :
       ∃ a : ℕ, x ≤ (2 : ℝ) ^ a ∧ (2 : ℝ) ^ a ≤ 2 * x ∧
         (a : ℝ) * Real.log 2 ≤ Real.log x + Real.log 2 := by
   …

2. theorem OAI.Problem337.ResidueConstruction.exists_binary_cutoff line 23
3. def OAI.Problem337.ResidueConstruction.auxiliaryDenominator line 31

   Source documentation

   The auxiliary denominator from one fixed block and a family of paired blocks.

   def auxiliaryDenominator {m R : ℕ} (a : ℕ) (p : Fin m → ℕ)
       (q : Fin R → Fin m → Fin 2 → ℕ) : ℕ :=
   …

4. def OAI.Problem337.ResidueConstruction.subsetEntry line 36

   Source documentation

   The fixed block enumerates all subset products.

   def subsetEntry {m : ℕ} (p : Fin m → ℕ) (I : Fin m → Fin 2) : ℕ :=
   …

5. def OAI.Problem337.ResidueConstruction.pairedEntry line 40

   Source documentation

   A paired block selects exactly one entry from every pair.

   def pairedEntry {m : ℕ} (q : Fin m → Fin 2 → ℕ) (I : Fin m → Fin 2) : ℕ :=
   …

6. theorem OAI.Problem337.ResidueConstruction.subsetEntry_dvd_product line 43
7. theorem OAI.Problem337.ResidueConstruction.prime_dvd_subsetEntry_iff line 51

   Source documentation

   A selected prime divides a fixed-block entry precisely when its bit is one.

   theorem prime_dvd_subsetEntry_iff {m : ℕ} (p : Fin m → ℕ)
       (hp : ∀ j, (p j).Prime) (hinj : Function.Injective p)
       (I : Fin m → Fin 2) (j : Fin m) :
       p j ∣ subsetEntry p I ↔ (I j).val = 1 := by
   …

   Mentions: OAI.Problem337.ResidueConstruction.subsetEntry

8. theorem OAI.Problem337.ResidueConstruction.subsetEntry_injective line 71

   Source documentation

   Distinct primes give all 2^m fixed-block entries distinct.

   theorem subsetEntry_injective {m : ℕ} (p : Fin m → ℕ)
       (hp : ∀ j, (p j).Prime) (hinj : Function.Injective p) :
       Function.Injective (subsetEntry p) := by
   …

   Mentions: OAI.Problem337.ResidueConstruction.subsetEntry

9. theorem OAI.Problem337.ResidueConstruction.subsetEntry_image_card line 84
10. theorem OAI.Problem337.ResidueConstruction.pairedEntry_dvd_product line 90
11. theorem OAI.Problem337.ResidueConstruction.binary_factor_dvd_auxiliary line 96
12. theorem OAI.Problem337.ResidueConstruction.ceiling_binary_factor_dvd_auxiliary line 102

    Source documentation

    Any covering binary factor also contains the precise ceiling cutoff used by terminal descent.

    theorem ceiling_binary_factor_dvd_auxiliary {m R : ℕ} (a D : ℕ) (p : Fin m → ℕ)
        (q : Fin R → Fin m → Fin 2 → ℕ) {S : ℝ} (hS : 0 < S)
        (hcut : S ^ D ≤ (2 : ℝ) ^ a) :
        2 ^ ⌈(D : ℝ) * Real.log S / Real.log 2⌉₊ ∣ auxiliaryDenominator a p q := by
    …

    Mentions: OAI.Problem337.D, OAI.Problem337.ResidueConstruction.auxiliaryDenominator

13. theorem OAI.Problem337.ResidueConstruction.subsetEntry_dvd_auxiliary line 114
14. theorem OAI.Problem337.ResidueConstruction.pairedEntry_dvd_auxiliary line 119
15. theorem OAI.Problem337.ResidueConstruction.auxiliaryDenominator_pos line 126
16. theorem OAI.Problem337.ResidueConstruction.subsetEntry_pos line 135
17. theorem OAI.Problem337.ResidueConstruction.pairedEntry_pos line 139
18. theorem OAI.Problem337.ResidueConstruction.log_nat_product line 143
19. theorem OAI.Problem337.ResidueConstruction.log_auxiliaryDenominator line 150
20. theorem OAI.Problem337.ResidueConstruction.log_auxiliaryDenominator_le line 182

    Source documentation

    The precise logarithmic size budget counts one fixed block and two factors per pair.

    theorem log_auxiliaryDenominator_le {m R : ℕ} (a : ℕ) (p : Fin m → ℕ)
        (q : Fin R → Fin m → Fin 2 → ℕ) (hp : ∀ j, 0 < p j)
        (hq : ∀ i j e, 0 < q i j e) (U : ℝ)
        (hpU : ∀ j, Real.log (p j : ℝ) ≤ U)
        (hqU : ∀ i j e, Real.log (q i j e : ℝ) ≤ U) :
        Real.log (auxiliaryDenominator a p q : ℝ) ≤
          (a : ℝ) * Real.log 2 + (2 * (R : ℝ) + 1) * (m : ℝ) * U := by
    …

    Mentions: OAI.Problem337.ResidueConstruction.auxiliaryDenominator

21. theorem OAI.Problem337.ResidueConstruction.log_auxiliaryDenominator_ge line 203
22. theorem OAI.Problem337.ResidueConstruction.log_pairedEntry_le line 220
23. theorem OAI.Problem337.ResidueConstruction.log_subsetEntry_le line 229
24. theorem OAI.Problem337.ResidueConstruction.residue_size_budget line 246

    Source documentation

    The numerical budgets have ample uniform slack. The floor-scale estimates are supplied separately, so this is pure algebra.

    theorem residue_size_budget {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 : ℝ) *
            (100 * Real.log S + Real.log 2) ≤ 204204 * S ∧
          (m : ℝ) * (100 * Real.log S + Real.log 2) ≤ 101 * S := by
    …

25. theorem OAI.Problem337.ResidueConstruction.auxiliaryDenominator_exp_bounds line 272

    Source documentation

    Explicit analytic inequalities imply the required exponential denominator window.

    theorem auxiliaryDenominator_exp_bounds {m R : ℕ} (a : ℕ) (p : Fin m → ℕ)
        (q : Fin R → Fin m → Fin 2 → ℕ) (hp : ∀ j, 0 < p j)
        (hq : ∀ i j e, 0 < q i j e) (S L U D : ℝ)
        (hpL : ∀ j, L ≤ Real.log (p j : ℝ))
        (hpU : ∀ j, Real.log (p j : ℝ) ≤ U)
        (hqU : ∀ i j e, Real.log (q i j e : ℝ) ≤ U)
        (hLower : S < (m : ℝ) * L)
        (hUpper : (a : ℝ) * Real.log 2 + (2 * (R : ℝ) + 1) * (m : ℝ) * U ≤ D * S) :
        Real.exp S < (auxiliaryDenominator a p q : ℝ) ∧
          (auxiliaryDenominator a p q : ℝ) ≤ Real.exp (D * S) := by
    …

    Mentions: OAI.Problem337.D, OAI.Problem337.ResidueConstruction.auxiliaryDenominator

26. theorem OAI.Problem337.ResidueConstruction.construct_residue_denominator line 297

    Source documentation

    Constructs the entire denominator-size/divisibility portion of the residue lemma. Only the prime-scale factor bounds and elementary floor-scale bounds are required here.

    theorem construct_residue_denominator {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 : ℝ) ≤ 100 * Real.log S + Real.log 2)
        (hqU : ∀ i j e, Real.log (q i j e : ℝ) ≤ 100 * Real.log S + Real.log 2) :
        ∃ 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