DensityFourierProduct.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Identifying the original density transform with its local prime factors

theorem OAI.Ostmann.intCast_isUnit_of_dvd line 11
theorem OAI.Ostmann.densityFourier_primeCRTFunction line 17
Source documentation
The multipliers produced by CRT are genuine units; they may be absorbed in the local arguments without imposing a new hypothesis on the density.
```
theorem densityFourier_primeCRTFunction (ps : List ℕ)
    (hp : ∀ p ∈ ps, p.Prime) (hc : ps.Pairwise Nat.Coprime)
    (f : ∀ p : ℕ, ZMod p → ℂ) :
    let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
…
```
Mentions: OAI.Ostmann.prime_list_prod_pos

theorem OAI.Ostmann.densityCRTList_value_eq_primeCRTFunction line 90

Source documentation

The recursively formed CRT density is exactly the product of the centered functions in the manuscript.

theorem densityCRTList_value_eq_primeCRTFunction (ps : List ℕ)
    (hp : ∀ p ∈ ps, p.Prime) (hc : ps.Pairwise Nat.Coprime)
    (S : ∀ p : ℕ, Finset (ZMod p)) :
    let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
…

Mentions: OAI.Ostmann.prime_list_prod_pos