FarHeightBound.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform height means pass through the far-cutoff Mellin integral. All frequency shifts are retained and the constant is independent of J.

lemma OAI.CubicFirstMoment.continuous_indexed_norm_polynomial line 13
lemma OAI.CubicFirstMoment.norm_indexed_norm_polynomial line 18
lemma OAI.CubicFirstMoment.far_norm_sum_norm_bound line 24
theorem OAI.CubicFirstMoment.far_norm_sum_height_bound line 37

theorem OAI.CubicFirstMoment.far_gauss_sum_height_bound line 67

Source documentation

Specialization to one coefficient at each Eisenstein integer.

theorem far_gauss_sum_height_bound (S : Finset Eisenstein) (c : Eisenstein → ℂ)
    (s x₀ : ℝ) {J T B : ℝ} (hJ : 0 < J) (hT : 0 < T)
    (hmean : ∀ v : ℝ, dyadicHeightMean
      (fun t => ‖∑ a ∈ S, c a*normTwist (t+v) a‖) T ≤ B) :
    dyadicHeightMean (fun t => ‖∑ a ∈ S, c a*normTwist (s+t) a*
      farInverseSquare (J*(Real.log (norm a)-x₀))‖) T ≤
      B*(∫ u : ℝ, ‖𝓕 farInverseSquare u‖) :=
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.dyadicHeightMean, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.farInverseSquare, OAI.CubicFirstMoment.norm