OAI/NumberTheory/JointDickman/Analysis/MellinLowFrequencyEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.angularMellinPolynomial_continuous line 10
2. lemma OAI.JointDickman.angularMellin_bounded_energy_le line 15
3. lemma OAI.JointDickman.angularMellin_bounded_energy_tendsto line 27
4. theorem OAI.JointDickman.weightedBin_low_frequency_energy line 53

   Source documentation

   The low-frequency energy of the bin labels and finite-prime weights tends to zero.

   theorem weightedBin_low_frequency_energy {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 →
         Tendsto (fun x : ℝ => ∫ τ in -T..T,
           ‖angularMellinPolynomial (Ioc ⌊A*x⌋₊ ⌊4*(A*x)⌋₊)
             (centeredWeightedBinCoefficient J ζ μ P t x) τ‖^2) atTop (𝓝 0) := by
   …

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