VaughanWeighted.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.Vaughan.weightedSum line 12
Source documentation
Finite complex weighted sum of a real arithmetic function.
```
def weightedSum (s : Finset ℕ) (w : ℕ → ℂ) (f : ArithmeticFunction ℝ) : ℂ :=
…
```
theorem OAI.Problem337.Vaughan.weightedSum_add line 15
theorem OAI.Problem337.Vaughan.weightedSum_sub line 20

theorem OAI.Problem337.Vaughan.weighted_identity line 26

Source documentation

Exact complex weighted Vaughan decomposition, using the canonical cutoff API.

theorem weighted_identity (s : Finset ℕ) (w : ℕ → ℂ) (U V : ℕ) :
    weightedSum s w Λ = weightedSum s w (shortPart V Λ) +
      weightedSum s w (shortPart U (μ : ArithmeticFunction ℝ) * ArithmeticFunction.log) -
      weightedSum s w (typeICoefficient U V * ζ) +
      weightedSum s w (typeIICoefficient U * longPart V Λ) := by
…

Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.shortPart, OAI.Problem337.Vaughan.typeICoefficient, OAI.Problem337.Vaughan.typeIICoefficient, OAI.Problem337.Vaughan.longPart

theorem OAI.Problem337.Vaughan.typeII_apply line 35
Source documentation
The Type II convolution is supported where both factors exceed the cutoffs.
```
theorem typeII_apply (U V n : ℕ) :
    (typeIICoefficient U * longPart V Λ) n =
      ∑ d ∈ n.divisorsAntidiagonal.filter (fun d => U < d.1 ∧ V < d.2),
        typeIICoefficient U d.1 * Λ d.2 := by
…
```
Mentions: OAI.Problem337.Vaughan.typeIICoefficient, OAI.Problem337.Vaughan.longPart
lemma OAI.Problem337.Vaughan.positive_interval line 46

theorem OAI.Problem337.Vaughan.weightedSum_mul line 52

Source documentation

A convolution sum with its outer coefficient factored out.

theorem weightedSum_mul (N : ℕ) (w : ℕ → ℂ) (f g : ArithmeticFunction ℝ) :
    weightedSum (Finset.Ioc 0 N) w (f * g) =
      ∑ a ∈ Finset.Ioc 0 N, (f a : ℂ) *
        ∑ b ∈ Finset.Ioc 0 (N / a), (g b : ℂ) * w (a * b) := by
…

Mentions: OAI.Problem337.Vaughan.weightedSum

theorem OAI.Problem337.Vaughan.weightedSum_mul_of_support line 60

Source documentation

A compactly supported coefficient restricts the outer interval exactly.

theorem weightedSum_mul_of_support (N A : ℕ) (w : ℕ → ℂ)
    (f g : ArithmeticFunction ℝ) (hf : ∀ a, A < a → f a = 0) :
    weightedSum (Finset.Ioc 0 N) w (f * g) =
      ∑ a ∈ Finset.Ioc 0 (min A N), (f a : ℂ) *
        ∑ b ∈ Finset.Ioc 0 (N / a), (g b : ℂ) * w (a * b) := by
…

Mentions: OAI.Problem337.Vaughan.weightedSum

theorem OAI.Problem337.Vaughan.first_typeI_eq_sum line 78

Source documentation

Exact first Type I sum with its actual short cutoff.

theorem first_typeI_eq_sum (N U : ℕ) (w : ℕ → ℂ) :
    weightedSum (Finset.Ioc 0 N) w
        (shortPart U (μ : ArithmeticFunction ℝ) * ArithmeticFunction.log) =
      ∑ a ∈ Finset.Ioc 0 (min U N), ((μ a : ℝ) : ℂ) *
        ∑ b ∈ Finset.Ioc 0 (N / a), (Real.log b : ℂ) * w (a * b) := by
…

Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.shortPart

theorem OAI.Problem337.Vaughan.second_typeI_eq_sum line 92

Source documentation

Exact second Type I sum, supported up to the product cutoff.

theorem second_typeI_eq_sum (N U V : ℕ) (w : ℕ → ℂ) :
    weightedSum (Finset.Ioc 0 N) w (typeICoefficient U V * ζ) =
      ∑ a ∈ Finset.Ioc 0 (min (U * V) N), (typeICoefficient U V a : ℂ) *
        ∑ b ∈ Finset.Ioc 0 (N / a), w (a * b) := by
…

Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.typeICoefficient