OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplatePair.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTemplatePairEquiv line 10
2. def OAI.Ostmann.movingTemplatePairSample line 14
3. theorem OAI.Ostmann.movingTemplatePairSample_left line 18
4. theorem OAI.Ostmann.movingTemplatePairSample_right line 22
5. theorem OAI.Ostmann.movingTemplatePairSample_small line 26
6. theorem OAI.Ostmann.movingTemplatePairSample_bulk line 49
7. theorem OAI.Ostmann.finite_prior_sum_type line 72
8. theorem OAI.Ostmann.movingTemplatePair_average line 93

   Source documentation

   Pairing surviving templates preserves the independent law. The shared compensation law stays outside this identity.

   theorem movingTemplatePair_average {A : Type*} [Fintype A] (n r m : ℕ)
       (ν : MovingRegularSlot (n + 1) r m → A → ℝ)
       (F : (MovingRegularSlot (n + 1) r m → A) → ℂ) :
       (∑ x, ((∏ i, ν i (x i) : ℝ) : ℂ) * F x) =
         ∑ left : MovingRegularSlot n r m → A,
           ((∏ i, ν (.inl i.1, i.2) (left i) : ℝ) : ℂ) *
             ∑ right : MovingRegularSlot n r m → A,
               ((∏ i, ν (.inr i.1, i.2) (right i) : ℝ) : ℂ) *
                 F (movingTemplatePairSample n r m left right) := by
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplatePairSample