OAI/NumberTheory/JointDickman/Amplification/FiniteAdditiveOrthogonality.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.additivePhase_conj line 12
2. theorem OAI.JointDickman.integral_additivePhase_int line 20
3. def OAI.JointDickman.finiteAdditiveSum line 37
4. theorem OAI.JointDickman.finiteAdditiveSum_continuous line 40
5. theorem OAI.JointDickman.integral_additive_pair line 46
6. theorem OAI.JointDickman.finiteAdditiveSum_pair_integral line 70

   Source documentation

   The exact finite Parseval pairing; different supports are allowed.

   theorem finiteAdditiveSum_pair_integral (s t : Finset ℕ) (c d : ℕ → ℂ) :
       (∫ θ in (0 : ℝ)..1, finiteAdditiveSum s c θ*conj (finiteAdditiveSum t d θ)) =
         ∑ n ∈ s, ∑ m ∈ t, if n = m then c n*conj (d m) else 0 := by
   …

   Mentions: OAI.JointDickman.finiteAdditiveSum

7. theorem OAI.JointDickman.finiteAdditiveSum_parseval line 97

   Source documentation

   Parseval for the finite trigonometric polynomials used in each box.

   theorem finiteAdditiveSum_parseval (s : Finset ℕ) (c : ℕ → ℂ) :
       (∫ θ in (0 : ℝ)..1, ‖finiteAdditiveSum s c θ‖^2) = ∑ n ∈ s, ‖c n‖^2 := by
   …

   Mentions: OAI.JointDickman.finiteAdditiveSum