OAI/NumberTheory/Ostmann/QuadraticCenter/SignedQuadraticFrequency.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.densityFourier_conj line 15
2. theorem OAI.Ostmann.primeDivisorDensity_conj line 21
3. theorem OAI.Ostmann.fourier_real_conj line 31

   Source documentation

   Reality of the original physical cutoff supplies Hermitian symmetry of its Fourier transform without any additional analytic input.

   theorem fourier_real_conj (f : ℝ → ℂ) (hf : ∀ x, conj (f x) = f x) (ξ : ℝ) :
       𝓕 f (-ξ) = conj (𝓕 f ξ) := by
   …

4. def OAI.Ostmann.integerQuadraticFrequency line 43
5. theorem OAI.Ostmann.integerQuadraticFrequency_natCast line 49
6. theorem OAI.Ostmann.integerQuadraticFrequency_neg line 59
7. theorem OAI.Ostmann.integerQuadraticFrequency_split line 72
8. theorem OAI.Ostmann.integerQuadraticFrequency_half_bound line 94