OAI/NumberTheory/Ostmann/Quadratic/QuadraticDensitySum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.quadraticDensityTerm line 11
2. def OAI.Ostmann.quadraticDensitySum line 17
3. def OAI.Ostmann.unitQuadraticSupport line 22
4. def OAI.Ostmann.quadraticUnitScalar line 27
5. theorem OAI.Ostmann.mem_unitQuadraticSupport line 32
6. theorem OAI.Ostmann.unitQuadraticSupport_subset line 37
7. theorem OAI.Ostmann.quadraticDensityTerm_nonunit line 42
8. theorem OAI.Ostmann.quadraticDensityTerm_eq_wave line 50
9. theorem OAI.Ostmann.quadraticDensitySum_eq_unit_waves line 66

   Source documentation

   Removing the zero nonunit terms leaves precisely the unit-wave sum to which the original-density correlation estimate applies.

   theorem quadraticDensitySum_eq_unit_waves {q : ℕ} [NeZero q] (g : ZMod q → ℂ)
       (hg : ∀ x, ¬IsUnit x → g x = 0) (W : Finset ℕ)
       (a : ZMod q) (θ : ℝ) (Φ : 𝓢(ℝ, ℂ)) (R v : ℝ) (s : ℕ)
       (hW : ∀ w ∈ W, 0 < w) (hR : 0 < R) (hv : 0 < v) :
       quadraticDensitySum g W a θ Φ R v s =
         normalizedDensityWaveSum g (unitQuadraticSupport W a) (quadraticUnitScalar a) Φ
           (fun w => θ * v * (w : ℝ) ^ 2 / q) (fun w => R * q / (v * (w : ℝ) ^ 2)) R v s := by
   …

   Mentions: OAI.Ostmann.quadraticDensitySum, OAI.Ostmann.normalizedDensityWaveSum, OAI.Ostmann.unitQuadraticSupport, OAI.Ostmann.quadraticUnitScalar