CompositeSupplyFinal.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.CompositeSupply.rational_divisor_sum_of_no_bad_divisor line 14
Source documentation
Absence of global bad conductors gives the actual eight-term rational representation in the ambient divisor pool.
```
lemma rational_divisor_sum_of_no_bad_divisor {Y q : ℕ}
    (hq : 0 < q) (hqY : q ≤ Y) (hc : q.Coprime (base Y))
    (hgood : ∀ d : ℕ, 2 ≤ d → d ∣ q → ¬ BadModulus d) :
    HasRationalDivisorSum (base Y ^ 2) (q : ℚ) 8 := by
…
```
Mentions: OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.HasRationalDivisorSum
theorem OAI.Problem337.CompositeSupply.eventually_supply_of_bad_multiples line 27
Source documentation
The entire remaining arithmetic input is the density bound for the specified global bad-divisor multiples.
```
theorem eventually_supply_of_bad_multiples
    (hbad : ∀ᶠ Y : ℕ in atTop,
      ((badCoprimeDivisorMultiples Y (base Y) (fun d => ¬ BadModulus d)).card : ℝ)
        < (Y : ℝ) / 12) :
    ∀ᶠ m : ℕ in atTop, HasRationalDivisorSupply m (multiplier m) 16 := by
…
```
Mentions: OAI.Problem337.badCoprimeDivisorMultiples, OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.HasRationalDivisorSupply, OAI.Problem337.CompositeSupply.multiplier
lemma OAI.Problem337.CompositeSupply.badCoprimeDivisorMultiples_subset_badMultiples line 41
Source documentation
The finite exception set used by cube-free density is contained in the single global logarithmic-tail exception set.
```
lemma badCoprimeDivisorMultiples_subset_badMultiples (Y : ℕ) :
    badCoprimeDivisorMultiples Y (base Y) (fun d => ¬ BadModulus d) ⊆
      badMultiples Y := by
…
```
Mentions: OAI.Problem337.badCoprimeDivisorMultiples, OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.CompositeSupply.badMultiples
theorem OAI.Problem337.CompositeSupply.eventually_supply_of_badMultiples_small line 52
Source documentation
Vanishing density of the actual global exceptional set suffices, with strict margin between one twenty-fourth and one twelfth.
```
theorem eventually_supply_of_badMultiples_small
    (hsmall : ∀ ε : ℝ, 0 < ε → ∀ᶠ Y : ℕ in atTop,
      ((badMultiples Y).card : ℝ) ≤ ε * Y) :
    ∀ᶠ m : ℕ in atTop, HasRationalDivisorSupply m (multiplier m) 16 := by
…
```
Mentions: OAI.Problem337.CompositeSupply.badMultiples, OAI.Problem337.HasRationalDivisorSupply, OAI.Problem337.CompositeSupply.multiplier
theorem OAI.Problem337.CompositeSupply.eventually_hasRationalDivisorSupply line 68
Source documentation
Unconditional sixteen-term supply for the explicit fourth-power prefix multiplier. Every arithmetic density and energy obligation is discharged.
```
theorem eventually_hasRationalDivisorSupply :
    ∀ᶠ m : ℕ in atTop, HasRationalDivisorSupply m (multiplier m) 16 :=
…
```
Mentions: OAI.Problem337.HasRationalDivisorSupply, OAI.Problem337.CompositeSupply.multiplier

theorem OAI.Problem337.CompositeSupply.quantitative_marked_length line 74

Source documentation

The exact marked Egyptian-fraction theorem, proved by the composite cube-free route without any prime-triple distribution premise.

theorem quantitative_marked_length :
    ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, 2 ≤ M ∧
      ∀ m : ℕ, M ≤ m → ∃ k : ℕ, ∃ n : Fin k → ℕ,
        IsOneExpansion n ∧ (∃ i, n i = m) ∧
        (k : ℝ) ≤ (257 / Real.log 2 + ε) * Real.log (Real.log (m : ℝ)) :=
…

Mentions: OAI.Problem337.IsOneExpansion