OAI/NumberTheory/Ostmann/Characters/CharacterWordSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.top_first_word_log_bounds line 11
2. theorem OAI.Ostmann.binnedWordAverage_support line 24
3. theorem OAI.Ostmann.supported_character_word_bounds line 37
4. theorem OAI.Ostmann.supported_character_bin_bounds line 59
5. theorem OAI.Ostmann.wordCopyPrior_word_support line 84

   Source documentation

   Nonzero mass for the complete two-copy tuple forces nonzero mass for both original word marginals.

   theorem wordCopyPrior_word_support {A : Type*} (k nc : ℕ)
       (μ : Fin k → A → ℝ) (ν : Fin nc → A → ℝ)
       (y : Fin ((k + nc) + (k + nc)) → A)
       (hy : productPrior (Fin.append (Fin.append μ ν) (Fin.append μ ν)) y ≠ 0) :
       productPrior μ ((wordCopyEquiv A k nc).symm y).1.1 ≠ 0 ∧
         productPrior μ ((wordCopyEquiv A k nc).symm y).2.1 ≠ 0 := by
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.wordCopyEquiv

6. theorem OAI.Ostmann.character_initial_word_support line 98
7. theorem OAI.Ostmann.character_select_supported_bin line 123