ThinSupplyBase.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.thinSupplyBase line 11
Source documentation
Prime-prefix supply with an arbitrary logarithmic coefficient.
```
def thinSupplyBase (a : ℝ) (u : ℕ) : ℕ :=
…
```
lemma OAI.Problem337.thinSupplyBase_pos line 14
lemma OAI.Problem337.thinSupplyBase_dvd_mono line 17
lemma OAI.Problem337.thinSupplyBase_fourth_power line 24
lemma OAI.Problem337.thinSupplyBase_sq_dvd_supplyInteger line 31
lemma OAI.Problem337.rpow_le_divisors_card_thinSupplyBase line 40
Source documentation
The exact divisor cardinality already dominates the real power dictated by its logarithmic prime-prefix coefficient.
```
lemma rpow_le_divisors_card_thinSupplyBase (a : ℝ) {u : ℕ} (hu : 0 < u) :
    (u : ℝ) ^ (a * Real.log 2) ≤ ((thinSupplyBase a u).divisors.card : ℝ) := by
…
```
Mentions: OAI.Problem337.thinSupplyBase
theorem OAI.Problem337.eventually_twice_rpow_le_divisors_card_thinSupplyBase line 57
Source documentation
Only a small power margin, not the manuscript's fourth-power overkill, is needed to ensure the factor-two collision-cardinality hypothesis.
```
theorem eventually_twice_rpow_le_divisors_card_thinSupplyBase
    (a θ : ℝ) (hgap : θ < a * Real.log 2) :
    ∀ᶠ u : ℕ in atTop,
      2 * (u : ℝ) ^ θ ≤ ((thinSupplyBase a u).divisors.card : ℝ) := by
…
```
Mentions: OAI.Problem337.thinSupplyBase

theorem OAI.Problem337.eventually_log_thinSupplyBase_le line 80

Source documentation

Sharp leading logarithmic size of the smaller prime-prefix base itself.

theorem eventually_log_thinSupplyBase_le (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) :
    ∀ᶠ u : ℕ in atTop,
      Real.log (thinSupplyBase a u : ℝ) ≤
        (a + ε) * Real.log (u : ℝ) * Real.log (Real.log (u : ℝ)) := by
…

Mentions: OAI.Problem337.thinSupplyBase

theorem OAI.Problem337.eventually_log_thinSupplyInteger_le line 88

Source documentation

The nested common multiplier has leading logarithmic size 8*a.

theorem eventually_log_thinSupplyInteger_le (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) :
    ∀ᶠ m : ℕ in atTop,
      Real.log (supplyInteger (4 * a) m : ℝ) ≤
        (8 * a + ε) * Real.log (m : ℝ) * Real.log (Real.log (m : ℝ)) := by
…

Mentions: OAI.Problem337.supplyInteger

lemma OAI.Problem337.lt_thinSupplyInteger line 95