OAI/NumberTheory/Ostmann/ZeroDensity/DensityCorrelationMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.norm_sum_le_of_energy line 11
2. theorem OAI.Ostmann.norm_product_sum_le_of_energy line 23
3. theorem OAI.Ostmann.correlationPrimeFactor_mass line 34
4. theorem OAI.Ostmann.primeCRTFunction_mass line 50
5. theorem OAI.Ostmann.primeSet_density_correlation_mass_model line 84

   Source documentation

   The original two density transforms have a common periodic model whose absolute mass is at most one after probability normalization.

   theorem primeSet_density_correlation_mass_model (U V : Finset ℕ)
       (hpU : ∀ p ∈ U, p.Prime) (hpV : ∀ p ∈ V, p.Prime)
       (S : ∀ p : ℕ, Finset (ZMod p))
       (vp : (ZMod U.toList.prod)ˣ) (vq : (ZMod V.toList.prod)ˣ) :
       let : NeZero U.toList.prod := ⟨(prime_list_prod_pos _ (primeSet_list_prime U hpU)).ne'⟩
   …

   Mentions: OAI.Ostmann.prime_list_prod_pos, OAI.Ostmann.primeSet_list_prime