ComplexShortIntervalConsequences.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The nonprincipal-character consequence of the published complex input

The arithmetic proof that the pretentious distance tends to infinity is a separate obligation. Given exactly that fact, the Matomäki--Radziwiłł--Tao input proves the short-average conclusion in the order of limits used in labels-short: the main scale tends to infinity before the short length.

def OAI.JointDickman.PublishedInputs.distanceError line 22
Source documentation
The pretentious-distance error in the published complex estimate.
```
noncomputable def distanceError (M : ℝ) : ℝ := (1 + M) * Real.exp (-M)
```
def OAI.JointDickman.PublishedInputs.shortLengthError line 25
Source documentation
The short-length error; it is fixed in the inner scale limit.
```
noncomputable def shortLengthError (H : ℝ) : ℝ :=
…
```
def OAI.JointDickman.PublishedInputs.longScaleError line 29
Source documentation
The long-scale error in the published complex estimate.
```
noncomputable def longScaleError (X : ℝ) : ℝ :=
…
```
theorem OAI.JointDickman.PublishedInputs.tendsto_distanceError line 32
theorem OAI.JointDickman.PublishedInputs.tendsto_shortLengthError line 40
theorem OAI.JointDickman.PublishedInputs.tendsto_longScaleError line 47
theorem OAI.JointDickman.PublishedInputs.tendsto_complex_error line 55
Source documentation
If all three parameters tend to infinity along one sequence, the complete right-hand side of the published complex estimate tends to zero.
```
theorem tendsto_complex_error {M H X : ℕ → ℝ}
    (hM : Tendsto M atTop atTop) (hH : Tendsto H atTop atTop)
    (hX : Tendsto X atTop atTop) (C : ℝ) :
    Tendsto (fun n => C * (distanceError (M n) + shortLengthError (H n) +
      longScaleError (X n))) atTop (𝓝 0) := by
…
```
Mentions: OAI.JointDickman.PublishedInputs.distanceError, OAI.JointDickman.PublishedInputs.shortLengthError, OAI.JointDickman.PublishedInputs.longScaleError

theorem OAI.JointDickman.PublishedInputs.complexShortAverage_eventually_eventually line 67

Source documentation

The exact iterated upper-limit conclusion for a nonprincipal-character summand. The sole number-theoretic hypotheses are the explicitly published complex input and divergence of its specified pretentious distance.

theorem complexShortAverage_eventually_eventually (hMRT : ComplexShortIntervalInput)
    (f : ℕ → ℕ → ArithmeticFunction ℂ)
    (hmult : ∀ B n, (f B n).IsMultiplicative)
    (hf : ∀ B n k, ‖f B n k‖ ≤ 1)
    (H : ℕ → ℝ) (X : ℕ → ℕ → ℝ)
    (hH : Tendsto H atTop atTop)
    (hX : ∀ B, Tendsto (X B) atTop atTop)
    (hdistance : ∀ B, Tendsto (fun n => minimumDistance (f B n) (X B n))
      atTop atTop) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ B in atTop, ∀ᶠ n in atTop,
      (1 / X B n) * (∫ z in X B n..2 * X B n,
        ‖complexShortAverage (f B n) (H B) z‖ ^ 2) < ε := by
…

Mentions: OAI.JointDickman.PublishedInputs.ComplexShortIntervalInput, OAI.JointDickman.PublishedInputs.minimumDistance, OAI.JointDickman.PublishedInputs.complexShortAverage