RationalSupplyReduction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.rational_divisor_sum_of_large_prime_image line 16
Source documentation
The five-product theorem and residue lifting give five rational divisors for every prime whose divisor-residue image is sufficiently large.
```
theorem rational_divisor_sum_of_large_prime_image (P p : ℕ) (hp : p.Prime)
    (hlarge : (p : ℝ) ^ (3 / 4 : ℝ) <
      (P.divisors.image (fun d : ℕ => (d : ZMod p))).card) :
    HasRationalDivisorSum (P ^ 2) (p : ℚ) 5 := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum
lemma OAI.Problem337.mod_image_card_eq_zmod_image_card line 29
def OAI.Problem337.supplyPrimeTriples line 36
Source documentation
Ordered prime triples of sum u, with their coordinates bounded by u.
```
def supplyPrimeTriples (u : ℕ) : Finset (ℕ × ℕ × ℕ) :=
…
```

theorem OAI.Problem337.rational_divisor_sum_of_many_prime_triples line 42

Source documentation

Actual collision counting and the five-product theorem reduce rational supply for a fixed integer to a lower bound for its number of prime triples.

theorem rational_divisor_sum_of_many_prime_triples (u P : ℕ)
    (hu : 2 ≤ u) (hP : 0 < P) (hsize : u ^ 4 ≤ P.divisors.card)
    (htriples : 6 * (u : ℝ) * (u : ℝ) ^ (3 / 4 : ℝ) *
      (Real.log (P : ℝ) / Real.log 2) < (supplyPrimeTriples u).card) :
    HasRationalDivisorSum (P ^ 2) (u : ℚ) 15 := by
…

Mentions: OAI.Problem337.supplyPrimeTriples, OAI.Problem337.HasRationalDivisorSum

def OAI.Problem337.QuantitativeThreePrimeLowerBound line 97
Source documentation
The precise external number-theoretic assertion used by this supply reduction. It is a proposition, not an axiom or an asserted theorem.
```
def QuantitativeThreePrimeLowerBound : Prop :=
…
```

theorem OAI.Problem337.eventually_rational_divisor_sum_of_three_prime_lower_bound line 103

Source documentation

Once quantitative three-prime input is provided, only elementary growth properties of the divisor-rich common products are needed for the odd supply.

theorem eventually_rational_divisor_sum_of_three_prime_lower_bound
    (P : ℕ → ℕ) (hthree : QuantitativeThreePrimeLowerBound)
    (hP : ∀ᶠ u : ℕ in atTop, 0 < P u ∧ u ^ 4 ≤ (P u).divisors.card)
    (hgrowth : ∃ C : ℝ, ∀ᶠ u : ℕ in atTop,
      Real.log (P u : ℝ) ≤ C * (Real.log (u : ℝ) * Real.log (Real.log (u : ℝ)))) :
    ∀ᶠ u : ℕ in atTop, Odd u →
      HasRationalDivisorSum ((P u) ^ 2) (u : ℚ) 15 := by
…

Mentions: OAI.Problem337.QuantitativeThreePrimeLowerBound, OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.eventually_full_rational_supply_of_odd line 142

Source documentation

Transfer the eventual odd-integer supply to every integer in the required initial interval, using nesting and eventual divisibility of each fixed range.

theorem eventually_full_rational_supply_of_odd
    (P K : ℕ → ℕ)
    (hodd : ∀ᶠ u : ℕ in atTop, Odd u →
      HasRationalDivisorSum ((P u) ^ 2) (u : ℚ) 15)
    (hnest : ∀ᶠ m : ℕ in atTop, ∀ u : ℕ, 1 ≤ u → u ≤ m ^ 4 → (P u) ^ 2 ∣ K m)
    (hsmall : ∀ N : ℕ, ∀ᶠ m : ℕ in atTop, ∀ s : ℕ, 1 ≤ s → s ≤ N → s ∣ K m) :
    ∀ᶠ m : ℕ in atTop, ∀ s : ℕ, 1 ≤ s → s ≤ m ^ 4 →
      HasRationalDivisorSum (K m) (s : ℚ) 16 := by
…

Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.eventually_full_rational_supply_of_three_prime_lower_bound line 168

Source documentation

Complete conditional supply reduction. Every ingredient other than the explicit three-prime lower bound is an elementary product-growth interface.

theorem eventually_full_rational_supply_of_three_prime_lower_bound
    (P K : ℕ → ℕ) (hthree : QuantitativeThreePrimeLowerBound)
    (hP : ∀ᶠ u : ℕ in atTop, 0 < P u ∧ u ^ 4 ≤ (P u).divisors.card)
    (hgrowth : ∃ C : ℝ, ∀ᶠ u : ℕ in atTop,
      Real.log (P u : ℝ) ≤ C * (Real.log (u : ℝ) * Real.log (Real.log (u : ℝ))))
    (hnest : ∀ᶠ m : ℕ in atTop, ∀ u : ℕ, 1 ≤ u → u ≤ m ^ 4 → (P u) ^ 2 ∣ K m)
    (hsmall : ∀ N : ℕ, ∀ᶠ m : ℕ in atTop, ∀ s : ℕ, 1 ≤ s → s ≤ N → s ∣ K m) :
    ∀ᶠ m : ℕ in atTop, ∀ s : ℕ, 1 ≤ s → s ≤ m ^ 4 →
      HasRationalDivisorSum (K m) (s : ℚ) 16 := by
…

Mentions: OAI.Problem337.QuantitativeThreePrimeLowerBound, OAI.Problem337.HasRationalDivisorSum