ConditionalMain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TotientAsymptotic.conditional_totient_scaling_of_structure line 14
Source documentation
Fixed-scale regular variation, proved using the same arithmetic mass at both endpoints. No continuity of the phase coefficient is required.
```
theorem conditional_totient_scaling_of_structure (hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) {c : ℝ} (hc : 0 < c) :
    Tendsto (fun x => V (c*x)/V x) atTop (nhds c) := by
…
```
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.V

theorem OAI.TotientAsymptotic.conditional_main_theorem_of_structure line 29

Source documentation

The complete main theorem of the supplied manuscript, conditional only on its precisely cited published inputs.

theorem conditional_main_theorem_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) ∧
    ∀ c : ℝ, 0 < c → Tendsto (fun x => V (c*x)/V x) atTop (nhds c) := by
…

theorem OAI.TotientAsymptotic.conditional_totient_scaling line 44
Source documentation
The original published-input interface remains available.
```
theorem conditional_totient_scaling (hscale : FordScaleBounds)
    (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) {c : ℝ} (hc : 0 < c) :
    Tendsto (fun x => V (c*x)/V x) atTop (nhds c) :=
…
```
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.V
theorem OAI.TotientAsymptotic.conditional_main_theorem line 51