OAI/NumberTheory/Ostmann/Arithmetic/BulkSymmetrization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.permuteBulk line 13
2. def OAI.Ostmann.bulkArrayEquiv line 16
3. def OAI.Ostmann.identicalBulkPrior line 22
4. theorem OAI.Ostmann.identicalBulkPrior_permute line 25
5. theorem OAI.Ostmann.bulk_value_product_permute line 30
6. def OAI.Ostmann.bulkSymmetrize line 35
7. theorem OAI.Ostmann.bulkSymmetrize_statistic line 41

   Source documentation

   The statistic is unchanged even if all bins and history restrictions are carried by F and have no permutation invariance.

   theorem bulkSymmetrize_statistic {I A : Type*} [Fintype I] [DecidableEq I] [Fintype A]
       (μ : A → ℝ) (G F : (I → A) → ℂ)
       (hG : ∀ e x, G (permuteBulk e x) = G x) :
       (∑ x : I → A, (identicalBulkPrior μ x : ℂ) * G x * bulkSymmetrize F x) =
         ∑ x : I → A, (identicalBulkPrior μ x : ℂ) * G x * F x := by
   …

   Mentions: OAI.Ostmann.permuteBulk, OAI.Ostmann.identicalBulkPrior, OAI.Ostmann.bulkSymmetrize

8. theorem OAI.Ostmann.bulkSymmetrize_cauchy line 67

   Source documentation

   Weighted Cauchy--Schwarz at the final symmetrized statistic.

   theorem bulkSymmetrize_cauchy {I A : Type*} [Fintype I] [DecidableEq I] [Fintype A]
       (μ : A → ℝ) (hμ : ∀ a, 0 ≤ μ a) (G F : (I → A) → ℂ) :
       ‖∑ x : I → A, (identicalBulkPrior μ x : ℂ) * G x * bulkSymmetrize F x‖ ^ 2 ≤
         (∑ x : I → A, identicalBulkPrior μ x * ‖G x‖ ^ 2) *
           ∑ x : I → A, identicalBulkPrior μ x * ‖bulkSymmetrize F x‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.identicalBulkPrior, OAI.Ostmann.bulkSymmetrize