OAI/NumberTheory/JointDickman/Analysis/MellinSampleDuality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.norm_finite_complex_pairing_sq line 15
2. theorem OAI.JointDickman.mellin_samples_of_dual line 24

   Source documentation

   Finite transpose duality, with no compactness or limiting argument.

   theorem mellin_samples_of_dual (P : Finset ℕ) (S : Finset ℝ)
       (a : ℕ → ℂ) {C : ℝ} (hC : 0 ≤ C)
       (hdual : ∀ b : ℝ → ℂ,
         (∑ n ∈ P, ‖∑ t ∈ S, b t *
           Complex.exp (((-Real.log (n : ℝ)*t : ℝ) : ℂ)*Complex.I)‖^2) ≤
             C*∑ t ∈ S, ‖b t‖^2) :
       (∑ t ∈ S, ‖mrtExponentialPolynomial P a (fun n => -Real.log (n : ℝ)) t‖^2) ≤
         C*∑ n ∈ P, ‖a n‖^2 := by
   …

3. def OAI.JointDickman.mellinSampleKernel line 63
4. lemma OAI.JointDickman.mellinSampleKernel_neg line 66
5. lemma OAI.JointDickman.mellin_weighted_dual_identity line 76
6. theorem OAI.JointDickman.mellin_weighted_dual_rows line 108

   Source documentation

   A row bound for the weighted Mellin kernel controls the dual quadratic form.

   theorem mellin_weighted_dual_rows (P : Finset ℕ) (S : Finset ℝ)
       (w : ℕ → ℝ) {C : ℝ}
       (hrow : ∀ t ∈ S, ∑ u ∈ S, ‖mellinSampleKernel P w (t-u)‖ ≤ C)
       (b : ℝ → ℂ) :
       (∑ n ∈ P, w n*‖∑ t ∈ S, b t *
         Complex.exp (((-Real.log (n : ℝ)*t : ℝ) : ℂ)*Complex.I)‖^2) ≤
           C*∑ t ∈ S, ‖b t‖^2 := by
   …

   Mentions: OAI.JointDickman.mellinSampleKernel