MetaplecticMellinMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Absolute Fubini for the metaplectic height average. The integrable majorant is deduced from the published mean square and the actual smooth Mellin transform; no contour identity is assumed.

lemma OAI.CubicFirstMoment.integral_height_norm_le line 16

Source documentation

A bound for the integral in the finite height variable is enough for absolute Fubini and a bound after integrating in the other variable.

lemma integral_height_norm_le (K : ℝ × ℝ → ℂ) (hK : Continuous K)
    {a b : ℝ} (hab : a ≤ b) (B : ℝ → ℝ) (hB : Integrable B)
    (hbound : ∀ v : ℝ, (∫ t in a..b, ‖K (v,t)‖) ≤ B v) :
    (∫ t in a..b, ‖∫ v : ℝ, K (v,t)‖) ≤ ∫ v : ℝ, B v := by
…

lemma OAI.CubicFirstMoment.mellin_linear_weight_integrable line 42

theorem OAI.CubicFirstMoment.metaplectic_mellin_height_mean line 59

Source documentation

The actual shifted Mellin integral satisfies the required square-root height mean. This step uses only HB's mean square, continuation on the integration line, and the decay of the chosen smooth weight.

theorem metaplectic_mellin_height_mean {F : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) (hHB : MetaplecticMeanSquare F)
    {ε : ℝ} (hε : 0 < ε) (hεsmall : ε < 1/12)
    (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Ioi 0) (hsm : ContDiff ℝ ∞ W) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ U : ℝ, 0 < U → ∀ T : ℝ, 1 ≤ T →
      (∫ t in -(2*T)..(2*T), ‖∫ v : ℝ,
        mellin W ((1/2+ε:ℝ)+(v:ℂ)*Complex.I)*
          (U:ℂ)^((1/2+ε:ℝ)+(v:ℂ)*Complex.I)*
          F r ((1/2+ε:ℝ)+((v-t):ℂ)*Complex.I)‖)/T ≤
        C*U^(1/2+ε)*(norm r)^(1/4+2*ε)*Real.sqrt T := by
…

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

theorem OAI.CubicFirstMoment.metaplectic_mellin_pole_decay line 118

Source documentation

The actual pole contribution has arbitrarily rapid height decay. Its level factor is the proved residue bound, with no divisor loss.

theorem metaplectic_mellin_pole_decay (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Ioi 0) (hsm : ContDiff ℝ ∞ W) (D : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ r : Eisenstein, primary r → ∀ U : ℝ, 0 < U → ∀ t : ℝ,
      ‖metaplecticResidue r*(U:ℂ)^((5/6:ℝ)+(t:ℂ)*Complex.I)*
        mellin W ((5/6:ℝ)+(t:ℂ)*Complex.I)‖ ≤
          C*U^(5/6:ℝ)*(norm r)^(-1/6:ℝ)/(1+|t|)^D := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticResidue, OAI.CubicFirstMoment.norm