OAI/NumberTheory/Ostmann/Construction/DoubledWordExpansion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.weighted_mean_norm_sq line 11
2. def OAI.Ostmann.jointWordPrior line 28
3. def OAI.Ostmann.jointWordAmplitude line 32
4. theorem OAI.Ostmann.joint_word_mean line 37
5. theorem OAI.Ostmann.jointWordAmplitude_norm_le_one line 57
6. theorem OAI.Ostmann.bounded_schwartz_real_correlation_summable line 73
7. theorem OAI.Ostmann.word_statistic_double_expansion line 92

   Source documentation

   Each role is sampled twice under its original law. Bin restrictions are indicators in the amplitude; the prior is never renormalized.

   theorem word_statistic_double_expansion {A B : Type*} [Fintype A] {k m : ℕ}
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (μ : Fin k → A → ℝ) (ν : Fin m → A → ℝ)
       (F : ℤ → Fin k → A → ℂ) (R : ℤ → Fin m → A → ℂ)
       (bin : (Fin k → A) → B) (b : B) (a : ℤ) :
       wordStatisticTerm ψ X (fun a => binnedWordAverage μ (F a) bin b)
         (fun i a => ∑ x, (ν i x : ℂ) * R a i x) a =
         (ψ ((a : ℝ) / X)).re *
           ∑ z, ∑ z', jointWordPrior μ ν z * jointWordPrior μ ν z' *
             (jointWordAmplitude (F a) (R a) bin b z *
               conj (jointWordAmplitude (F a) (R a) bin b z')).re := by
   …

   Mentions: OAI.Ostmann.wordStatisticTerm, OAI.Ostmann.binnedWordAverage, OAI.Ostmann.jointWordPrior, OAI.Ostmann.jointWordAmplitude

8. theorem OAI.Ostmann.word_statistic_tsum_double_expansion line 115

   Source documentation

   The finite original prime averages commute with the physical Schwartz sum. No conditioning or change of prior occurs in this expansion.

   theorem word_statistic_tsum_double_expansion {A B : Type*} [Fintype A] {k m : ℕ}
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X)
       (μ : Fin k → A → ℝ) (ν : Fin m → A → ℝ)
       (F : ℤ → Fin k → A → ℂ) (R : ℤ → Fin m → A → ℂ)
       (hF : ∀ a i x, ‖F a i x‖ ≤ 1) (hR : ∀ a i x, ‖R a i x‖ ≤ 1)
       (bin : (Fin k → A) → B) (b : B) :
       (∑' a : ℤ, wordStatisticTerm ψ X (fun a => binnedWordAverage μ (F a) bin b)
         (fun i a => ∑ x, (ν i x : ℂ) * R a i x) a) =
         ∑ z, ∑ z', jointWordPrior μ ν z * jointWordPrior μ ν z' *
           ∑' a : ℤ, (ψ ((a : ℝ) / X)).re *
             (jointWordAmplitude (F a) (R a) bin b z *
               conj (jointWordAmplitude (F a) (R a) bin b z')).re := by
   …

   Mentions: OAI.Ostmann.wordStatisticTerm, OAI.Ostmann.binnedWordAverage, OAI.Ostmann.jointWordPrior, OAI.Ostmann.jointWordAmplitude