OAI/NumberTheory/Ostmann/Construction/InitialWordExpectation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_prior_reindex line 11
2. theorem OAI.Ostmann.prime_product_reindex line 19
3. theorem OAI.Ostmann.mem_wordCharacterEvent line 24
4. theorem OAI.Ostmann.wordGraphAmplitude_univ line 33
5. theorem OAI.Ostmann.initial_prime_expectation_reindex line 57

   Source documentation

   Reindexing changes no original marginal and no prime-pairwise test.

   theorem initial_prime_expectation_reindex {I : Type*} [Fintype I] [DecidableEq I] {n : ℕ}
       (e : I ≃ Fin n) (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (Q : Fin n → Finset ℕ) (χ : Fin n → ∀ p : ℕ, DirichletCharacter ℂ p)
       (t : ∀ p : ℕ, ZMod p) (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (N : ℕ)
       (R : (I → P) → Prop) [DecidablePred R] :
       (∑ x : I → P, ((∏ i, primeSubsetPrior P (Q (e i)) (x i) : ℝ) : ℂ) *
         if Pairwise (fun i j => (x i : ℕ).Coprime (x j : ℕ)) ∧
             R x then
           sampledTupleAmplitude P hP (fun i => χ (e i)) t ψ X N x else 0) =
       ∑ x : Fin n → P, (productPrior (fun j => primeSubsetPrior P (Q j)) x : ℂ) *
         if Function.Injective x ∧ R (fun i => x (e i)) then
           sampledTupleAmplitude P hP χ t ψ X N x else 0 := by
   …

   Mentions: OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.sampledTupleAmplitude, OAI.Ostmann.productPrior