SeedConsequences.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TotientAsymptotic.seeds_one_two line 11
Source documentation
The arithmetic seed assertion requires no published hypothesis.
```
theorem seeds_one_two : ∀ k∈({1,2} : Finset ℕ),
    ∃ d : ℕ, IsTotient d ∧ k*d<ell d :=
…
```
Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell
theorem OAI.TotientAsymptotic.companion_one_two_without_seed_input_of_structure line 16
Source documentation
The k=1,2 weighted conclusions after discharging the finite seed input.
```
theorem companion_one_two_without_seed_input_of_structure (hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput)
    (hppt : ∀ d : ℕ, IsTotient d → PPTBoundedFiberPropagation d) :
    ∀ k∈({1,2} : Finset ℕ), ∃ c : ℝ, 0<c ∧
      ∀ s∈Set.Ico (0 : ℝ) 1, c≤A (fk k) s :=
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.PPTBoundedFiberPropagation, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.fk
theorem OAI.TotientAsymptotic.companion_one_two_without_seed_input line 28
Source documentation
The original published-input interface remains available.
```
theorem companion_one_two_without_seed_input (hscale : FordScaleBounds)
    (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput)
    (hppt : ∀ d : ℕ, IsTotient d → PPTBoundedFiberPropagation d) :
    ∀ k∈({1,2} : Finset ℕ), ∃ c : ℝ, 0<c ∧
      ∀ s∈Set.Ico (0 : ℝ) 1, c≤A (fk k) s :=
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.FordTheorem10Input, OAI.TotientAsymptotic.FordTheorem16Input, OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.PPTBoundedFiberPropagation, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.fk