AngularDyadicMoment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact finite dyadic splitting of the retained dual integral and the resulting character-average bound.

def OAI.CubicFirstMoment.finiteAngularDualIntegral line 14
lemma OAI.CubicFirstMoment.finiteAngularIdealDualIntegral_dyad_partition line 20

theorem OAI.CubicFirstMoment.angular_retained_ideal_dyadic_moment_transfer line 47

Source documentation

A bound for each actual normalized ideal dyad transfers to the whole retained integral with only its finite number of dyads lost.

theorem angular_retained_ideal_dyadic_moment_transfer
    (k : ℝ) (hk : 0 ≤ k)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ {ι : Type*} [Fintype ι], ∀ (S : Finset EisensteinIdealExponent)
      (χ : ι → EisensteinIdealExponent → ℂ) (ε : ι → ℂ) (A : ι → ℝ),
      (∀ i, ‖ε i‖ = 1) → (∀ i, 0 < A i) → ∀ (Z t : ℝ) (B : ℕ → ℝ),
      1 ≤ Z → (∀ j ∈ idealDyadIndices S, 0 ≤ B j) →
      (∀ j ∈ idealDyadIndices S, ∀ τ : ℝ,
        (∑ i, ‖normalizedDualPolynomial (idealDyad S j) (χ i) idealExponentNorm
          ((2:ℝ)^j) (τ-t)‖^2) ≤ B j) →
      (∑ i, ‖finiteAngularDualIntegral W S (χ i) idealExponentNorm (ε i) (A i) k Z t‖^2) ≤
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealDyadIndices, OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.idealDyad, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.finiteAngularDualIntegral