OAI/NumberTheory/Ostmann/Arithmetic/MovingSeparatedProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingFrequencyPairSupport line 10
2. def OAI.Ostmann.movingFrequencyPairFactor line 17
3. def OAI.Ostmann.movingSpectatorPairFactor line 27
4. theorem OAI.Ostmann.movingSeparatedPairResidueCoefficient_product line 35

   Source documentation

   The coefficient of the literal original pair is a product over disjoint arithmetic blocks. No Haar averaging or independence is assumed here.

   theorem movingSeparatedPairResidueCoefficient_product {σ I : Type*} (q : I → ℕ)
       [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       (g : ∀ i, ZMod (q i) → ℂ) (D : Bool → ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       {n : ℕ} (T : Bool → MovingSlotData σ n) (nodes : Bool → List MovingFormulaNode)
       (R : ℤ) (P : Finset ℕ)
       (hcover : ∀ side, ∀ o ∈ (T side).occurrences,
         ∀ i ∈ o.current.compensationSlots, value i ∈ P) (x y : ℕ) :
       movingSeparatedPairResidueCoefficient q value outside F E g D S T nodes R x y =
         movingFrequencyPairFactor value outside F E T nodes R x y *
           (∏ p ∈ P, movingInternalPairFactor value T p x y) *
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.movingSeparatedPairResidueCoefficient, OAI.Ostmann.movingFrequencyPairFactor, OAI.Ostmann.movingInternalPairFactor