IteratedLogBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Erdos970.NumberTheoryLean.IteratedLogBound.of_source_root_lower line 17

Source documentation

The strengthened main follows from the same precise survivor estimate as the old quadratic main. No strengthened conclusion is assumed here.

theorem of_source_root_lower (c : ℝ) (hc : 0 < c)
    (z : ℝ → PrimeHistories.Node)
    (hLower : ∀ᶠ top : ℝ in atTop, ∀ a : ℕ → ℕ,
      c * ((ErdosInverseBoxHeight.sourceY top : ℝ) *
        SmallSieveFinite.smallEuler ⌊ErdosInverseBoxHeight.sourceW top⌋₊ /
        (ErdosInverseBoxHeight.sourceB top) ^ 2) ≤
      countSurvivors (ErdosInverseBoxHeight.sourceY top)
        (LargePrimeDeletion.cutoffPrimes ⌊ErdosInverseBoxHeight.sourceW top⌋₊) a
        (rootVertex (z top) ∅ (sourcePrimeSet (ErdosInverseBoxHeight.sourceW top) top)
          ((ErdosInverseBoxHeight.sourceY top : ℝ) *
            SmallSieveFinite.smallEuler ⌊ErdosInverseBoxHeight.sourceW top⌋₊))) :
    Targets.JacobsthalIteratedLog := by
…

Mentions: OAI.Erdos970.NumberTheoryLean.PrimeHistories.Node, OAI.Erdos970.ErdosInverseBoxHeight.sourceY, OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.smallEuler, OAI.Erdos970.ErdosInverseBoxHeight.sourceW, OAI.Erdos970.ErdosInverseBoxHeight.sourceB, OAI.Erdos970.NumberTheoryLean.LargePrimeDeletion.cutoffPrimes, OAI.Erdos970.NumberTheoryLean.Targets.JacobsthalIteratedLog

theorem OAI.Erdos970.Erdos970Final.erdos_970_iterated_log line 59
Source documentation
Manuscript 293, strengthened Theorem 1.1, revision ad16712e7b45.
Distinct definitions of this name: ComparatorChallenges/JacobsthalImproved.lean:22 (same statement text; different proof or body). Qualify references as OAI.Erdos970.Erdos970Final.erdos_970_iterated_log@path.
```
theorem erdos_970_iterated_log : NumberTheoryLean.Targets.JacobsthalIteratedLog := by
…
```
Mentions: OAI.Erdos970.NumberTheoryLean.Targets.JacobsthalIteratedLog