AngularSmoothApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform smooth dual approximation at each fixed infinity type, derived from the precise published completion and classical Gamma inputs. The original sum retains every primitive local Euler factor.

def OAI.CubicFirstMoment.angularRetainedIntegral line 13

theorem OAI.CubicFirstMoment.angular_smooth_approximation line 22

Source documentation

Uniform arbitrary-power approximation beyond the natural dual length. The original sum and retained integral are explicitly defined.

theorem angular_smooth_approximation
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {k : ℝ} (hk : 0 ≤ k) {δ : ℝ} (hδ : 0 < δ) (B R : ℝ) :
    ∃ (m : ℕ) (C : ℝ), 2 ≤ m ∧ 0 ≤ C ∧
      ∀ (χ χdual : EisensteinIdealExponent → ℂ),
      (∀ ν, ‖χ ν‖ ≤ 1) → (∀ ν, ‖χdual ν‖ ≤ 1) →
      ∀ (ε : ℂ), ‖ε‖ ≤ 1 → ∀ (Y A Z J t : ℝ),
      1 ≤ Y → 0 < A → 1 ≤ Z → 0 < J → Z ≤ Y^B → J ≤ Y^B →
      (A^2*(1+|t|)^2)/(Z*J) ≤ Y^(-δ) →
      ∀ (L Ldual : ℂ → ℂ), ShiftedPrimitiveHeckeAnalyticData χ χdual A k ε L Ldual →
      ShiftedCompletedHeckeFiniteOrder A k L →
      AngularGammaQuotientStripBound k (1/2-(m:ℝ)) →
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.ShiftedPrimitiveHeckeAnalyticData, OAI.CubicFirstMoment.ShiftedCompletedHeckeFiniteOrder, OAI.CubicFirstMoment.AngularGammaQuotientStripBound

theorem OAI.CubicFirstMoment.primitive_angular_smooth_approximation line 56

Source documentation

Actual primitive angular characters satisfy the proved approximation. The constant is chosen before the modulus, character, root and lengths.

theorem primitive_angular_smooth_approximation (hpub : PrimitiveAngularHeckeInput)
    (ℓ : ℤ) (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {δ : ℝ} (hδ : 0 < δ) (H R : ℝ)
    (hGI : ∀ m : ℕ, GammaInverseFiniteOrder
      (1/2-(m:ℝ)+|(ℓ:ℝ)|/2) (2+|(ℓ:ℝ)|/2))
    (hGQ : ∀ m : ℕ, AngularGammaQuotientStripBound (|(ℓ:ℝ)|/2) (1/2-(m:ℝ))) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (q : Eisenstein), q ≠ 0 →
      ∀ χ : MulChar (Residues q) ℂ, PrimitiveResidueCharacter q χ →
      AngularUnitCompatible q χ ℓ → (ℓ ≠ 0 ∨ χ ≠ 1) →
      ∃ root : ℂ, ‖root‖ = 1 ∧ ∀ (Y Z J t : ℝ),
      1 ≤ Y → 1 ≤ Z → 0 < J → Z ≤ Y^H → J ≤ Y^H →
      ((residueHeckeScale q)^2*(1+|t|)^2)/(Z*J) ≤ Y^(-δ) →
…

Mentions: OAI.CubicFirstMoment.PrimitiveAngularHeckeInput, OAI.CubicFirstMoment.GammaInverseFiniteOrder, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.AngularUnitCompatible, OAI.CubicFirstMoment.residueHeckeScale