MultiplicativeExtraction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Extracting a fixed divisor from two ordinary multiplicative functions. The failure of coprimality is counted explicitly, including its finite interval boundary term.

def OAI.TwoPointCorrelations.multiplicativeExtractionGap line 15
lemma OAI.TwoPointCorrelations.multiplicativeExtractionGap_eq_zero line 18
lemma OAI.TwoPointCorrelations.norm_multiplicativeExtractionGap_le line 28
theorem OAI.TwoPointCorrelations.multiplicativeExtraction_sum_bound line 52

theorem OAI.TwoPointCorrelations.weightedMultiplicativeExtraction_sum_bound line 76

Source documentation

Bounded cutoffs and progression indicators may be inserted before the absolute value; their dependence on the integer is unrestricted.

theorem weightedMultiplicativeExtraction_sum_bound {f g : ℕ → ℂ}
    (hfm : Multiplicative f) (hgm : Multiplicative g)
    (hf : OneBounded f) (hg : OneBounded g)
    (u d Y : ℕ) (hu : 0 < u) (P : Finset ℕ)
    (hP : ∀ p ∈ P, Nat.Prime p)
    (hcover : ∀ p, Nat.Prime p → p ∣ u → p ∈ P)
    (q : ℕ → ℂ) (K : ℝ) (hK : 0 ≤ K) (hq : ∀ n, 0 < n → ‖q n‖ ≤ K) :
    ‖positivePrefix (fun n => q n * multiplicativeExtractionGap f g u d n) Y‖ ≤
      K * (4 * (Y : ℝ) * (∑ p ∈ P, 1 / (p : ℝ)) + 4 * P.card) := by
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.positivePrefix, OAI.TwoPointCorrelations.multiplicativeExtractionGap

theorem OAI.TwoPointCorrelations.finiteShift_extraction_sum_bound line 105

Source documentation

Arbitrary finite shift families retain only their coefficient mass; the exceptional-residue bound is uniform in the chosen shifts.

theorem finiteShift_extraction_sum_bound {ι : Type*} {f g : ℕ → ℂ}
    (hfm : Multiplicative f) (hgm : Multiplicative g)
    (hf : OneBounded f) (hg : OneBounded g)
    (u Y : ℕ) (hu : 0 < u) (P : Finset ℕ)
    (hP : ∀ p ∈ P, Nat.Prime p)
    (hcover : ∀ p, Nat.Prime p → p ∣ u → p ∈ P)
    (S : Finset ι) (a : ι → ℂ) (d : ι → ℕ) (q : ι → ℕ → ℂ)
    (K : ℝ) (hK : 0 ≤ K) (hq : ∀ i ∈ S, ∀ n, 0 < n → ‖q i n‖ ≤ K) :
    ‖∑ i ∈ S, a i * positivePrefix (fun n => q i n * multiplicativeExtractionGap f g u (d i) n) Y‖ ≤
      (∑ i ∈ S, ‖a i‖) *
        (K * (4 * (Y : ℝ) * (∑ p ∈ P, 1 / (p : ℝ)) + 4 * P.card)) := by
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.positivePrefix, OAI.TwoPointCorrelations.multiplicativeExtractionGap

theorem OAI.TwoPointCorrelations.multiplicativeExtraction_average_bound line 129
lemma OAI.TwoPointCorrelations.primeReciprocalSum_le_card_div line 145
theorem OAI.TwoPointCorrelations.multiplicativeExtraction_rough_bound line 155