OAI/NumberTheory/JointDickman/Amplification/BinLowFrequency.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Unconditional low-frequency control of the actual weighted bin labels

  1. lemma OAI.JointDickman.norm_binLabel_le_one_of_norm_le line 12
  2. lemma OAI.JointDickman.binDistributionMean_norm_le_one_of_norm_le line 25
  3. def OAI.JointDickman.centeredWeightedBinCoefficient line 46
  4. lemma OAI.JointDickman.centeredWeightedBinCoefficient_norm line 51
  5. theorem OAI.JointDickman.weightedBin_low_frequency line 67

    Source documentation

    The one-variable bin law, already proved in this development, suffices for every bounded angular-frequency interval. The mean is independent of all subsequent finite-prime restrictions.

    theorem weightedBin_low_frequency {J : ℕ} (hJ : 2 ≤ J)
    (ζ : Fin (J-1) → ℂ) (hζ : ∀ i, ‖ζ i‖ ≤ 1) :
    ∃ μ : ℂ, ‖μ‖ ≤ 1 ∧ ∀ (P : Finset ℕ), (∀ p ∈ P, p.Prime) →
      ∀ t : ℕ → ℝ, (∀ p ∈ P, 0 ≤ t p ∧ t p ≤ 1) →
      ∀ A T ε : ℝ, 0 < A → 0 ≤ T → 0 < ε →
      ∀ᶠ x : ℝ in atTop, ∀ τ : ℝ, |τ| ≤ T →
        ‖angularMellinPolynomial (Ioc ⌊A * x⌋₊ ⌊4 * (A * x)⌋₊)
          (centeredWeightedBinCoefficient J ζ μ P t x) τ‖ ≤ ε := by
…

    Mentions: OAI.JointDickman.angularMellinPolynomial, OAI.JointDickman.centeredWeightedBinCoefficient