AngularDualTail.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The fixed-angular far-left tail, with explicit natural dual length. Only the constant changes with the angular shift; every power of the length, conductor and height is retained from the full ideal series.

def OAI.CubicFirstMoment.angularDualTailIntegrand line 16
Source documentation
The integrand of the omitted part of the functional-equation series on the line Re s = 1/2-m.
```
def angularDualTailIntegrand (W : ℝ → ℂ) (χ : EisensteinIdealExponent → ℂ)
    (ε : ℂ) (A Z J k : ℝ) (m : ℕ) (t τ : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.norm_angularDualTailIntegrand_le line 23

theorem OAI.CubicFirstMoment.angular_dual_tail_integral_bound line 80

Source documentation

An arbitrary-order tail bound with the natural dual length displayed. The constant depends only on the fixed weight and the chosen order m.

theorem angular_dual_tail_integral_bound (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Ioi 0) (hsm : ContDiff ℝ ∞ W)
    {k : ℝ} (hk : 0 ≤ k) {m : ℕ} (hm : 2 ≤ m) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (χ : EisensteinIdealExponent → ℂ),
      (∀ ν, ‖χ ν‖ ≤ 1) → ∀ (ε : ℂ), ‖ε‖ ≤ 1 →
      ∀ (A Z J : ℝ), 0 < A → 0 < Z → 0 < J → ∀ t : ℝ,
      ‖∫ τ : ℝ, angularDualTailIntegrand W χ ε A Z J k m t τ‖ ≤
        C*Z^(1/2:ℝ)*J^(3/2:ℝ)*((A^2*(1+|t|)^2)/(Z*J))^m := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.angularDualTailIntegrand

theorem OAI.CubicFirstMoment.angular_dual_tail_arbitrary_power line 128

Source documentation

The omitted far-left tail is smaller than every fixed negative power once the cutoff exceeds the natural length by Y^δ. Only polynomial upper bounds for the two lengths are used.

theorem angular_dual_tail_arbitrary_power (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 ∧
      ∀ (χ : EisensteinIdealExponent → ℂ), (∀ ν, ‖χ ν‖ ≤ 1) →
      ∀ (ε : ℂ), ‖ε‖ ≤ 1 → ∀ (Y A Z J : ℝ),
      1 ≤ Y → 0 < A → 0 < Z → 0 < J → Z ≤ Y^B → J ≤ Y^B →
      ∀ t : ℝ, (A^2*(1+|t|)^2)/(Z*J) ≤ Y^(-δ) →
      ‖∫ τ : ℝ, angularDualTailIntegrand W χ ε A Z J k m t τ‖ ≤ C*Y^(-R) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.angularDualTailIntegrand