MultiplicativeBessel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact finite-character orthogonality step in the ordinary large sieve.

lemma OAI.CubicFirstMoment.mulChar_gram line 15
theorem OAI.CubicFirstMoment.mulChar_bessel line 27
Source documentation
Bessel inequality for any selected finite set of distinct multiplicative characters, with the exact unit-group cardinality.
```
theorem mulChar_bessel (C : Finset (MulChar R ℂ)) (v : R → ℂ) :
    (∑ χ ∈ C, ‖∑ x : R, v x*χ x‖^2) ≤
      (Fintype.card Rˣ:ℝ)*∑ x : R, ‖v x‖^2 := by
…
```

theorem OAI.CubicFirstMoment.gauss_transform_bessel line 41

Source documentation

Gauss expansion transfers a character family to its additive sums without a conductor loss. The hypotheses are finite Fourier identities, not an analytic large-sieve estimate.

theorem gauss_transform_bessel {ι : Type*} (N : Finset ι)
    (C : Finset (MulChar R ℂ)) (v : ι → ℂ)
    (phase : R → ι → ℂ) (t : MulChar R ℂ → ι → ℂ)
    (g : MulChar R ℂ → ℂ)
    (hR : 0 < Fintype.card R)
    (hg : ∀ χ ∈ C, ‖g χ‖^2 = Fintype.card R)
    (htransform : ∀ χ ∈ C, ∀ n ∈ N,
      g χ*t χ n = ∑ x : R, χ x*phase x n) :
    (∑ χ ∈ C, ‖∑ n ∈ N, v n*t χ n‖^2) ≤
      ∑ x : R, ‖∑ n ∈ N, v n*phase x n‖^2 := by
…

theorem OAI.CubicFirstMoment.gauss_transform_unit_bessel line 85

Source documentation

The same transfer with the additive side restricted to units. This is the restriction appearing in the published additive large sieve.

theorem gauss_transform_unit_bessel {ι : Type*} (N : Finset ι)
    (C : Finset (MulChar R ℂ)) (v : ι → ℂ)
    (phase : R → ι → ℂ) (t : MulChar R ℂ → ι → ℂ)
    (g : MulChar R ℂ → ℂ)
    (hR : 0 < Fintype.card R)
    (hg : ∀ χ ∈ C, ‖g χ‖^2 = Fintype.card R)
    (htransform : ∀ χ ∈ C, ∀ n ∈ N,
      g χ*t χ n = ∑ x : R, χ x*phase x n) :
    (∑ χ ∈ C, ‖∑ n ∈ N, v n*t χ n‖^2) ≤
      ∑ x : R, if IsUnit x then ‖∑ n ∈ N, v n*phase x n‖^2 else 0 := by
…