OAI/NumberTheory/Ostmann/Construction/PrimePhysicalTest.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.normalizedResidueIndicator_energy_le line 12

   Source documentation

   Degenerate residue sets give the zero normalized test. Thus the energy bound holds before a balanced-prime restriction is inserted.

   theorem normalizedResidueIndicator_energy_le {p : ℕ} [NeZero p]
       (S : Finset (ZMod p)) :
       (∑ x, ‖normalizedResidueIndicator S x‖ ^ 2) ≤ (p : ℝ) := by
   …

   Mentions: OAI.Ostmann.normalizedResidueIndicator

2. def OAI.Ostmann.primePhysicalTest line 37

   Source documentation

   A giant uses the Fourier phase on favorable primes and zero elsewhere; every other prime position uses the exact normalized residue indicator.

   noncomputable def primePhysicalTest {p : ℕ} [NeZero p]
       (S : Finset (ZMod p)) (giant favorable : Bool) : ZMod p → ℂ :=
   …

3. theorem OAI.Ostmann.primePhysicalTest_sum line 43
4. theorem OAI.Ostmann.primePhysicalTest_energy line 50
5. theorem OAI.Ostmann.primePhysicalTest_bound line 61
6. theorem OAI.Ostmann.primePhysicalTest_real line 66
7. theorem OAI.Ostmann.primePhysicalTest_fourier line 75