UniformHeightMellin.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A translation-uniform height mean passes through the whole Mellin line without truncation. All interchanges follow from absolute Fubini.

lemma OAI.CubicFirstMoment.dyadicHeightMean_convolution_uniform line 13

theorem OAI.CubicFirstMoment.arithmeticMellin_signed_height_uniform line 35

Source documentation

Both signs of the arithmetic Mellin coefficient have the same full line bound. The sole cost is its already proved zeroth moment.

theorem arithmeticMellin_signed_height_uniform (M : ℝ) (hM : 0 < M) (V : ℝ → ℂ)
    (hV : HasCompactSupport V) (hV' : ContDiff ℝ ∞ V) (q : ℕ) :
    ∃ D : ℝ, 0 < D ∧ ∀ ρ : ℝ, 0 ≤ ρ →
      ∀ (G : ℝ → ℝ), Continuous G → ∀ (E B T u ε : ℝ),
      (ε = 1 ∨ ε = -1) → 0 ≤ B → 0 < T → (∀ t, ‖G t‖ ≤ E) →
      (∀ v, dyadicHeightMean (fun t => G (t+v)) T ≤ B) →
      (1+ρ)^q*dyadicHeightMean (fun t => ∫ s : ℝ,
        ‖arithmeticMellinCoefficient M hM V hV hV' ρ (ε*s)‖*G (t+u+s)) T ≤ D*B := by
…

Mentions: OAI.CubicFirstMoment.dyadicHeightMean, OAI.CubicFirstMoment.arithmeticMellinCoefficient