TypeIHeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Derivations of the integrated height bound from the metaplectic mean square.

lemma OAI.CubicFirstMoment.continuous_interval_cauchy line 12

Source documentation

Cauchy on a finite real interval, with the interval length explicit.

lemma continuous_interval_cauchy (f : ℝ → ℂ) (hf : Continuous f)
    {a b : ℝ} (hab : a ≤ b) :
    (∫ t in a..b, ‖f t‖)^2 ≤ (b-a)*(∫ t in a..b, ‖f t‖^2) := by
…

theorem OAI.CubicFirstMoment.translated_metaplectic_square line 34

Source documentation

Translate the actual mean square to any frequency window before integrating against the Mellin transform.

theorem translated_metaplectic_square {F : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) (hHB : MetaplecticMeanSquare F)
    {ε : ℝ} (hε : 0 < ε) (hεsmall : ε < 1/12) :
    ∃ C : ℝ, 0 < C ∧ ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ T : ℝ, 1 ≤ T → ∀ v : ℝ,
      (∫ t in -(2*T)..(2*T), ‖F r ((1/2+ε:ℝ)+((v-t):ℂ)*Complex.I)‖^2) ≤
        C*(norm r)^(1/2+4*ε)*(2*T+|v|+1)^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticContinuation, OAI.CubicFirstMoment.MetaplecticMeanSquare, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.translated_metaplectic_mean line 60

Source documentation

Averaged first moment on a translated height window. The complete frequency dependence is retained for the subsequent Mellin integration.

theorem translated_metaplectic_mean {F : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) (hHB : MetaplecticMeanSquare F)
    {ε : ℝ} (hε : 0 < ε) (hεsmall : ε < 1/12) :
    ∃ K : ℝ, 0 < K ∧ ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ T : ℝ, 1 ≤ T → ∀ v : ℝ,
      (∫ t in -(2*T)..(2*T), ‖F r ((1/2+ε:ℝ)+((v-t):ℂ)*Complex.I)‖)/T ≤
        K*(norm r)^(1/4+2*ε)*(3+|v|)*Real.sqrt T := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticContinuation, OAI.CubicFirstMoment.MetaplecticMeanSquare, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm