DualPolynomialScale.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The exact sqrt(Z/J) normalization of a retained dual norm block. The normalized coefficients are independent of the character conductor.

lemma OAI.CubicFirstMoment.positive_cpow_phase line 12
lemma OAI.CubicFirstMoment.dual_dyad_weight_identity line 22
lemma OAI.CubicFirstMoment.dual_dyad_weight_le_one line 27

theorem OAI.CubicFirstMoment.finite_dual_dyad_rescale line 36

Source documentation

Extracting the inverse square-root dyadic length changes only the fixed norm coefficients; the character remains in the same polynomial.

theorem finite_dual_dyad_rescale {ι : Type*} (S : Finset ι) (a : ι → ℂ)
    (N : ι → ℝ) {J : ℝ} (hJ : 0 < J) (hN : ∀ i ∈ S, 0 < N i) (u : ℝ) :
    finiteNormDirichlet S a N ((1/2:ℂ)-(u:ℂ)*Complex.I) =
      (J^(-(1/2:ℝ)):ℝ)*∑ i ∈ S,
        (a i*((J/N i)^(1/2:ℝ):ℝ))*mellinPhase u (N i) := by
…

Mentions: OAI.CubicFirstMoment.finiteNormDirichlet, OAI.CubicFirstMoment.mellinPhase

lemma OAI.CubicFirstMoment.norm_dual_dyad_coefficient_le line 52