OAI/NumberTheory/JointDickman/Analysis/MellinRestrictionEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.angularMellin_restriction_error_energy line 11
2. theorem OAI.JointDickman.angularMellin_restriction_energy line 51

   Source documentation

   The cutoff costs its ordinary density, uniformly on every frequency subset of a fixed polynomial-length interval.

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

   Mentions: OAI.JointDickman.angularMellinPolynomial