OAI/NumberTheory/Ostmann/Arithmetic/BulkFrequencyRepresentative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingFrequencyCore_bulk_residues line 14

   Source documentation

   Once the nonbulk coordinates have been fixed, the frequency factor is a function of the frequency-unit array alone. The representative does not alter any compensation denominator.

   theorem movingFrequencyCore_bulk_residues {σ J : Type*}
       (value : σ → ℕ) (e : J ↪ σ) (r : ℕ) [NeZero r]
       (a : J → (ZMod r)ˣ) (ha : ∀ j, (value (e j) : ZMod r) = (a j : ZMod r))
       (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       {n : ℕ} (T : Bool → MovingSlotData σ n) (R : ℤ)
       (hf : ∀ b, (T b).Frequencies (· ≠ 0))
       (hT : ∀ b j, (T b).CompensationAbsent (e j))
       (hR : ∀ b, (T b).frequencyProduct ∣ R) (hr : R ^ (n + 1) ∣ (r : ℤ))
       (XL XR : ℤ) :
       movingFrequencyCore value F E T R XL XR =
         movingFrequencyCore (Function.extend e (fun j => (a j).val.val) value) F E T R XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFrequencyCore