OAI/NumberTheory/Ostmann/Arithmetic/GroupedBulkSymmetrization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.selectedBulkAverage_statistic line 11
2. theorem OAI.Ostmann.groupedCoefficient_bulk_average line 41

   Source documentation

   All pointwise cutoffs may remain inside the coefficient. Only the key and the original independent bulk law are invariant under reassignment.

   theorem groupedCoefficient_bulk_average {B A K : Type*} [Fintype B] [Fintype A]
       (n m : ℕ) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (ν : B → A → ℝ) (hν : ∀ j k, ν (slot j) = ν (slot k))
       (key : (B → A) → K) (hkey : ∀ e y, key (selectedBulkSample slot e y) = key y)
       (W : (B → A) → ℂ) (k : K) :
       groupedCoefficient key (fun y => ((∏ i, ν i (y i) : ℝ) : ℂ) *
         mixedBulkSymmetrize n m slot (fun _ y _ _ => W y) 0 y 0 0) k =
       groupedCoefficient key (fun y => ((∏ i, ν i (y i) : ℝ) : ℂ) * W y) k := by
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.selectedBulkSample, OAI.Ostmann.groupedCoefficient, OAI.Ostmann.mixedBulkSymmetrize