ShortMoebiusFinite.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Finite primary ideal polynomials and their actual Eisenstein-element realizations. These sums omit the ramified prime above three. They are not identified with the complete ideal series of IdealMellinSeries.

lemma OAI.CubicFirstMoment.idealExponentOf_eq_of_associated line 15
lemma OAI.CubicFirstMoment.idealExponentOf_primaryGenerator line 21
lemma OAI.CubicFirstMoment.idealPrimaryGenerator_injective line 28
def OAI.CubicFirstMoment.primaryElementBall line 32
Source documentation
Primary element sums omit every ideal divisible by the prime over three.
```
def primaryElementBall (Y : ℝ) : Finset Eisenstein :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.mem_primaryElementBall line 35
def OAI.CubicFirstMoment.primaryIdealBall line 46
Source documentation
The corresponding finite ideal set, explicitly restricted to ideals with a primary generator, hence prime to the ramified prime.
```
def primaryIdealBall (Y : ℝ) : Finset EisensteinIdealExponent :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.mem_primaryIdealBall line 49
lemma OAI.CubicFirstMoment.primaryIdealBall_coprime_three line 62
def OAI.CubicFirstMoment.primaryIdealPolynomial line 70
Source documentation
The primary ideal character polynomial with an arbitrary arithmetic coefficient function.
```
def primaryIdealPolynomial (Y : ℝ) (A : EisensteinArithmeticFunction)
    (χ : Eisenstein → ℂ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein
theorem OAI.CubicFirstMoment.primaryIdealPolynomial_eq_elements line 74
theorem OAI.CubicFirstMoment.shortIdealPolynomial_eq_moebius line 91
Source documentation
The short factor is the literal bounded Möbius polynomial over primary elements. No complete ideal series or ramified Euler factor is inserted.
```
theorem shortIdealPolynomial_eq_moebius (F : ℝ) (χ : Eisenstein → ℂ) :
    primaryIdealPolynomial (Real.sqrt F) (shortIdealMoebius F) χ =
      ∑ a ∈ primaryElementBall (Real.sqrt F), (idealMoebius a : ℂ)*χ a := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.shortIdealMoebius, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.idealMoebius
lemma OAI.CubicFirstMoment.logIdealPolynomial_eq_elements line 102
lemma OAI.CubicFirstMoment.zetaIdealPolynomial_eq_elements line 111
lemma OAI.CubicFirstMoment.primaryCharacter_prod line 116

theorem OAI.CubicFirstMoment.primaryIdealPolynomial_product line 131

Source documentation

Independent ideal factors are exactly the collected actual element convolution. Each factor may have its own complex norm weight.

theorem primaryIdealPolynomial_product {ι : Type*} [Fintype ι] [DecidableEq ι]
    (Y : ι → ℝ) (A : ι → EisensteinArithmeticFunction) (w : ι → Eisenstein → ℂ)
    (χ : Eisenstein → ℂ) (hχ1 : χ 1 = 1)
    (hχ : ∀ x y, primary x → primary y → χ (x*y) = χ x*χ y) :
    (∏ i, primaryIdealPolynomial (Y i) (A i) (fun a => w i a*χ a)) =
      ∑ b ∈ orderedConvolutionSupport (fun i => primaryElementBall (Y i)),
        orderedConvolution (fun i => primaryElementBall (Y i))
          (fun i a => ((MvPowerSeries.coeff (idealExponentOf a) (A i) : ℝ) : ℂ)*w i a) b * χ b := by
…

Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.idealExponentOf

lemma OAI.CubicFirstMoment.primaryIdealBall_generator_mem line 154
lemma OAI.CubicFirstMoment.primaryIdealBall_card_le line 159
lemma OAI.CubicFirstMoment.primaryIdealPolynomial_norm_le line 166
theorem OAI.CubicFirstMoment.shortIdealPolynomial_norm_le line 178
Source documentation
The short Möbius polynomial has the actual half-length trivial bound.
```
theorem shortIdealPolynomial_norm_le (F : ℝ) (χ : Eisenstein → ℂ)
    (hχ : ∀ a ∈ primaryElementBall (Real.sqrt F), ‖χ a‖ ≤ 1) :
    ‖primaryIdealPolynomial (Real.sqrt F) (shortIdealMoebius F) χ‖ ≤ 18*Real.sqrt F := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.shortIdealMoebius
theorem OAI.CubicFirstMoment.logIdealPolynomial_norm_le line 186
Source documentation
The full primary log polynomial has a uniform elementary norm bound.
```
theorem logIdealPolynomial_norm_le {Y : ℝ} (hY : 1 ≤ Y) (χ : Eisenstein → ℂ)
    (hχ : ∀ a ∈ primaryElementBall Y, ‖χ a‖ ≤ 1) :
    ‖primaryIdealPolynomial Y idealLogNorm χ‖ ≤ 18*Y*Real.log Y := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.idealLogNorm
lemma OAI.CubicFirstMoment.zetaIdealPolynomial_norm_le line 194