DischargedMain.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Joint distributions from progressively weaker analytic hypotheses

theorem OAI.JointDickman.main_results_after_mertens line 16
theorem OAI.JointDickman.main_results_after_elementary_inputs line 27

theorem OAI.JointDickman.main_results_after_bin_distribution line 38

Source documentation

The exact main results after the two Mertens estimates, finite concentration, and finite-bin Dickman distribution have been proved.

theorem main_results_after_bin_distribution
    (hMR : RealShortIntervalInput) (hMRT : ComplexShortIntervalInput)
    (hKMT : CharacterDistanceInput) (hFord : FordUpperSieveInput)
    (hSD : SquarefreeSelbergDelangeInput) (hSW : SquarefreeCharacterEstimateInput)
    (hMV : MultiplicativeExponentialInput) :
    JointDickmanLaw ∧ IncreasingOrderLaw ∧ DecreasingOrderLaw :=
…

Mentions: OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.IncreasingOrderLaw, OAI.JointDickman.DecreasingOrderLaw

theorem OAI.JointDickman.main_results_after_upper_sieve line 49

Source documentation

All three exact main results with the two Mertens estimates, concentration, finite-bin distribution, and the finite-event upper sieve discharged.

theorem main_results_after_upper_sieve
    (hMR : RealShortIntervalInput) (hMRT : ComplexShortIntervalInput)
    (hKMT : CharacterDistanceInput)
    (hSD : SquarefreeSelbergDelangeInput) (hSW : SquarefreeCharacterEstimateInput)
    (hMV : MultiplicativeExponentialInput) :
    JointDickmanLaw ∧ IncreasingOrderLaw ∧ DecreasingOrderLaw :=
…

Mentions: OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.IncreasingOrderLaw, OAI.JointDickman.DecreasingOrderLaw

theorem OAI.JointDickman.main_results_after_selberg_delange line 59
Source documentation
The exact main results after the squarefree Selberg--Delange expansion has also been proved, including every fixed order and all real cutoffs.
```
theorem main_results_after_selberg_delange
    (hMR : RealShortIntervalInput) (hMRT : ComplexShortIntervalInput)
    (hKMT : CharacterDistanceInput) (hSW : SquarefreeCharacterEstimateInput)
    (hMV : MultiplicativeExponentialInput) :
    JointDickmanLaw ∧ IncreasingOrderLaw ∧ DecreasingOrderLaw :=
…
```
Mentions: OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.IncreasingOrderLaw, OAI.JointDickman.DecreasingOrderLaw
theorem OAI.JointDickman.main_results_after_character_estimate line 68
Source documentation
The exact main results after the uniform squarefree character estimate has also been proved for both fixed exponents and every real cutoff.
```
theorem main_results_after_character_estimate
    (hMR : RealShortIntervalInput) (hMRT : ComplexShortIntervalInput)
    (hKMT : CharacterDistanceInput) (hMV : MultiplicativeExponentialInput) :
    JointDickmanLaw ∧ IncreasingOrderLaw ∧ DecreasingOrderLaw :=
…
```
Mentions: OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.IncreasingOrderLaw, OAI.JointDickman.DecreasingOrderLaw
theorem OAI.JointDickman.main_results_after_character_distance line 76
Source documentation
All three exact main results using the proved qualitative character-distance bound. The stronger numerical KMT input is no longer required.
```
theorem main_results_after_character_distance
    (hMR : RealShortIntervalInput) (hMRT : ComplexShortIntervalInput)
    (_hMV : MultiplicativeExponentialInput) :
    JointDickmanLaw ∧ IncreasingOrderLaw ∧ DecreasingOrderLaw := by
…
```
Mentions: OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.IncreasingOrderLaw, OAI.JointDickman.DecreasingOrderLaw
theorem OAI.JointDickman.main_results_after_exponential_sums line 89
Source documentation
The exact joint law and both ordering laws after the necessary Montgomery--Vaughan minor-arc special case has been proved.
```
theorem main_results_after_exponential_sums
    (hMR : RealShortIntervalInput) (hMRT : ComplexShortIntervalInput) :
    JointDickmanLaw ∧ IncreasingOrderLaw ∧ DecreasingOrderLaw := by
…
```
Mentions: OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.IncreasingOrderLaw, OAI.JointDickman.DecreasingOrderLaw