MetaplecticInverseMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite inverse completion transfers actual signed-height means. The weight norm is estimated pointwise; its height-dependent phase is retained in the exact identity and never treated as constant.

lemma OAI.CubicFirstMoment.continuous_metaplecticAngularSmoothSum_of_cutoff line 16
lemma OAI.CubicFirstMoment.metaplectic_inverse_pointwise_norm line 28
lemma OAI.CubicFirstMoment.metaplectic_inverse_interval_norm line 44

theorem OAI.CubicFirstMoment.metaplectic_inverse_signed_mean line 71

Source documentation

The only loss in inverse completion is the actual finite harmonic norm sum. The completed-mean premise is discharged by the published-input angular bound in the subsequent application.

theorem metaplectic_inverse_signed_mean
    (r : Eisenstein) (ℓ : ℤ) (W : ℝ → ℂ) (hWc : HasCompactSupport W)
    {U B F T H : ℝ} (hU : 0 < U) (hB : 0 ≤ B) (hBF : B*U ≤ F)
    (hW : ∀ x : ℝ, B < x → W x = 0) (hT : 0 < T)
    (hmean : ∀ c ∈ primaryElementBall F,
      ((∫ t in -(2*T)..-T, ‖metaplecticHeightCompleted r ℓ W (U/norm c^3) t‖)+
        (∫ t in T..2*T, ‖metaplecticHeightCompleted r ℓ W (U/norm c^3) t‖))/T ≤
          H*Real.sqrt (U/norm c^3)) :
    ((∫ t in -(2*T)..-T, ‖metaplecticAngularSmoothSum r ℓ W U t‖)+
      (∫ t in T..2*T, ‖metaplecticAngularSmoothSum r ℓ W U t‖))/T ≤
        H*Real.sqrt U*(∑ c ∈ primaryElementBall F, norm c^(-1:ℝ)) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.metaplecticHeightCompleted, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticAngularSmoothSum