OAI/NumberTheory/Ostmann/Arithmetic/MovingOriginalPatternSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPatternInjectionGuard line 10
2. theorem OAI.Ostmann.movingPatternInjectionGuard_norm line 15
3. theorem OAI.Ostmann.movingPatternInjectionGuard_nonzero line 24
4. theorem OAI.Ostmann.movingOriginalPattern_sum_fin line 35

   Source documentation

   The original dependent pattern coefficient with independent external priors is exactly the full finite-coordinate sum with this support mask.

   theorem movingOriginalPattern_sum_fin {A B C : Type*}
       [Fintype A] [Fintype B] [Fintype C] {N : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
       (prime : A → ℕ) (n : ℕ) (pattern : Bool × MovingSampleIndex n → C)
       (G : (Fin (N + 1) → A) → ℂ) :
       (∑ y : B → A, ∑ z : {z : C → A // Function.Injective z},
         ((∏ b, ν b (y b) : ℝ) : ℂ) *
           (internalPatternWeight pattern (fun i => μ (movingSampleTier i.2)) prime z.val : ℂ) *
           G (fun i => Sum.elim y z.val (e i))) =
       ∑ x : Fin (N + 1) → A, ((∏ b, ν b (x (e.symm (.inl b))) : ℝ) : ℂ) *
         (movingPairCompensatedMass μ prime ((movingSamplePairCoordinates A n).symm
           (fun i => x (e.symm (.inr (pattern i))))) : ℂ) * movingPatternInjectionGuard e G x := by
   …

   Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.internalPatternWeight, OAI.Ostmann.movingSampleTier, OAI.Ostmann.movingPairCompensatedMass, OAI.Ostmann.movingSamplePairCoordinates, OAI.Ostmann.movingPatternInjectionGuard