OAI/NumberTheory/Ostmann/Construction/PrimeWordInitialAmplitude.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_word_fixed_bin_amplitude line 10
2. theorem OAI.Ostmann.prime_word_fixed_bin_amplitude_norm line 53

   Source documentation

   The original character amplitude requires no common phase convention.

   theorem prime_word_fixed_bin_amplitude_norm {B : Type*}
       (k nc : ℕ) (hk : 0 < k) (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (Q : Fin k → Finset ℕ) (R : Fin nc → Finset ℕ)
       (hQ : ∀ i, Q i ⊆ P) (hR : ∀ i, R i ⊆ P)
       (hQmass : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
       (hRmass : ∀ i, (∑ p ∈ R i, (p : ℝ)⁻¹) ≠ 0)
       (χ : ∀ p : ℕ, DirichletCharacter ℂ p) (hχ : ∀ p ∈ P, χ p ≠ 1)
       (t : ∀ p : ℕ, ZMod p) (E : Finset ℤ)
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X)
       (bin : (Fin k → P) → B) (b : B) (c ρ γ : ℝ)
       (hρ : 0 ≤ ρ) (hγ : 0 ≤ γ)
       (hψ : ∀ x, 0 ≤ (ψ x).re) (hreal : ∀ x, (ψ x).im = 0)
   …