AmplifiedProfile.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Nonzero arithmetic correlations survive smooth amplification

theorem OAI.JointDickman.amplification_norm_lower line 12

theorem OAI.JointDickman.smooth_amplified_profile_lower line 29

Source documentation

The positive lower constant is independent of the later fixed regularity cutoff. The outer limit is still conditional only on the cited analytic inputs.

theorem smooth_amplified_profile_lower
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput)
    (W : ResidueProfile) (hW : W.mean ≠ 0) :
    ∃ d : ℝ, 0 < d ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
      ∃ C₀ : ℝ, 0 ≤ C₀ ∧ ∀ C : ℝ, C₀ ≤ C → ∀ T : ℕ → ℕ,
        (∀ᶠ B : ℕ in atTop, 0 < T B ∧ (T B : ℝ) ≤ Real.exp ((1/10 : ℝ)*B)) →
        ∀ᶠ B : ℕ in atTop, d * ‖W.mean‖ ≤
          ‖W.correlation (amplificationPeriod B) (smoothResidueAmplification B L τ C (T B))‖ := by
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.ResidueProfile, OAI.JointDickman.amplificationPeriod, OAI.JointDickman.smoothResidueAmplification

theorem OAI.JointDickman.exists_arithmetic_amplification_profile line 55

Source documentation

A single extracted subsequence supplies all the inner arithmetic limits. The profile and its bounds are constructed from the bounded array.

theorem exists_arithmetic_amplification_profile (H : ℕ → ℕ → ℂ) {C : ℝ}
    (hC : 0 ≤ C) (hH : ∀ N n, ‖H N n‖ ≤ C) {β : ℂ}
    (hmean : Tendsto (fun N => (∑ n ∈ range N, H N n) / (N : ℂ)) atTop (nhds β)) :
    ∃ (s : ℕ → ℕ), StrictMono s ∧ ∃ W : ResidueProfile, W.mean = β ∧
      ∀ (B L : ℕ) (τ C' : ℝ) (T : ℕ),
        Tendsto (fun N => (∑ n ∈ range (s N), H (s N) n *
          (arithmeticSubsetAmplification B L τ C' (amplificationSmoothWeight B T) n : ℂ)) / (s N : ℂ))
          atTop (nhds (W.correlation (amplificationPeriod B)
            (smoothResidueAmplification B L τ C' T))) := by
…

Mentions: OAI.JointDickman.ResidueProfile, OAI.JointDickman.arithmeticSubsetAmplification, OAI.JointDickman.amplificationSmoothWeight, OAI.JointDickman.amplificationPeriod, OAI.JointDickman.smoothResidueAmplification