ArbitraryHeightMean.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Ordinary height means for arbitrary primary coefficient supports, including sharp norm cells and every translated angular mode.

lemma OAI.CubicFirstMoment.continuous_finite_character_height line 13

theorem OAI.CubicFirstMoment.finite_character_height_mean line 23

Source documentation

Exact norm-fiber cost for the finite family. Character factors can only reduce the coefficient energy.

theorem finite_character_height_mean {C M T : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) (hM : 0 ≤ M) (hT : 0 < T)
    (B H : Finset Eisenstein) (β : Eisenstein → ℂ) (Z : ℕ)
    (hB : ∀ b ∈ B, primary b)
    (hZ : ∀ b ∈ B, normNat b ∈ Finset.Icc 1 Z)
    (hmult : ∀ n ∈ Finset.Icc 1 Z, ((B.filter (fun b => normNat b = n)).card:ℝ) ≤ M)
    (ℓ : ℤ) (u : ℝ) :
    dyadicHeightMean (fun t => ∑ h ∈ H,
      ‖∑ b ∈ B, β b*cubicSymbol b h*theta ℓ b*mellinPhase (t+u) (norm b)‖^2) T ≤
      2*C*(1+(Z:ℝ)/T)*M*H.card*∑ b ∈ B, ‖β b‖^2 := by
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.dyadicHeightMean, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.theta, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.arbitrary_primary_height_mean line 58

Source documentation

With no fixed number of prime factors, the proved primary norm-fiber bound gives an arbitrarily small length loss, uniformly in all twists.

theorem arbitrary_primary_height_mean {C ε : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) (hε : 0 < ε) :
    ∃ D : ℝ, 0 < D ∧ ∀ (B H : Finset Eisenstein) (β : Eisenstein → ℂ) (Z : ℕ),
      (∀ b ∈ B, primary b) → (∀ b ∈ B, normNat b ∈ Finset.Icc 1 Z) →
      ∀ (ℓ : ℤ) (u T : ℝ), 0 < T →
      dyadicHeightMean (fun t => ∑ h ∈ H,
        ‖∑ b ∈ B, β b*cubicSymbol b h*theta ℓ b*mellinPhase (t+u) (norm b)‖^2) T ≤
        2*C*D*(1+(Z:ℝ)/T)*(Z:ℝ)^ε*H.card*∑ b ∈ B, ‖β b‖^2 := by
…