OAI/NumberTheory/JointDickman/Analysis/TypicalMellinLowFrequency.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.angularMellinPolynomial_sub line 11
2. lemma OAI.JointDickman.norm_angularMellinPolynomial_le line 18
3. lemma OAI.JointDickman.angularMellin_restriction_difference line 26
4. theorem OAI.JointDickman.angularMellin_restriction_low_energy line 56

   Source documentation

   Cutting out a set of small ordinary density preserves the bounded frequency estimate, with an explicit squared counting error.

   theorem angularMellin_restriction_low_energy (E : ℕ → Prop) (f b : ℕ → ℂ)
       (hf : ∀ n, ‖f n‖ ≤ 1) {N K : ℕ} (hN : 0 < N) {T : ℝ} (hT : 0 ≤ T) :
       (∫ t in -T..T, ‖angularMellinPolynomial (Ioc N K)
         (fun n => (if E n then f n else 0)-b n) t‖^2) ≤
         2*(∫ t in -T..T, ‖angularMellinPolynomial (Ioc N K) (fun n => f n-b n) t‖^2) +
         4*T*((((Ioc N K).filter fun n => ¬E n).card : ℝ)/N)^2 := by
   …

   Mentions: OAI.JointDickman.angularMellinPolynomial