ConditionalAsymptotic.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The unweighted asymptotic, conditional only on the precisely cited published inputs. All tuple, collision, mass and coverage estimates are proved.

theorem OAI.TotientAsymptotic.conditional_totient_asymptotic_of_structure line 15

Source documentation

The main asymptotic and its finite arithmetic coefficient.

theorem conditional_totient_asymptotic_of_structure (hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput) :
    TendstoUniformlyOn (fun H => AH H (fun _ => 1)) (A (fun _ => 1))
      atTop (Set.Ico (0 : ℝ) 1) ∧
    (∃ cMinus cPlus : ℝ, 0<cMinus ∧ ∀ s ∈ Set.Ico (0 : ℝ) 1,
      cMinus ≤ A (fun _ => 1) s ∧ A (fun _ => 1) s ≤ cPlus) ∧
    Tendsto (fun x => V x/mainTerm x) atTop (nhds 1) := by
…

theorem OAI.TotientAsymptotic.conditional_totient_asymptotic line 40
Source documentation
The original published-input interface remains available.
```
theorem conditional_totient_asymptotic (hscale : FordScaleBounds)
    (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput) :
    TendstoUniformlyOn (fun H => AH H (fun _ => 1)) (A (fun _ => 1))
      atTop (Set.Ico (0 : ℝ) 1) ∧
    (∃ cMinus cPlus : ℝ, 0<cMinus ∧ ∀ s ∈ Set.Ico (0 : ℝ) 1,
      cMinus ≤ A (fun _ => 1) s ∧ A (fun _ => 1) s ≤ cPlus) ∧
    Tendsto (fun x => V x/mainTerm x) atTop (nhds 1) :=
…
```
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.AH, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.mainTerm