OAI/NumberTheory/Ostmann/Arithmetic/BulkFrequencyResidues.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotData.CompensationAgreement line 11
2. theorem OAI.Ostmann.MovingSlotData.compensationAgreement_of_eq_off line 18
3. theorem OAI.Ostmann.naturalProduct_modEq_values line 32
4. theorem OAI.Ostmann.MovingSlotReversal.signedNumerator_values_modEq line 42
5. theorem OAI.Ostmann.MovingSlotReversal.frequencyPivot_values_modEq line 50
6. theorem OAI.Ostmann.movingFrequencyGate_values_modEq line 68

   Source documentation

   All frequency divisibility and unit tests survive simultaneous bulk replacement. Only one frequency power is consumed at each tree level.

   theorem movingFrequencyGate_values_modEq {σ : Type*} (v w : σ → ℕ) (R : ℤ)
       {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0))
       (hcomp : T.CompensationAgreement v w) (hR : T.frequencyProduct ∣ R)
       (hv : ∀ i, (v i : ℤ) ≡ (w i : ℤ) [ZMOD R ^ (n + 1)])
       (XL XR YL YR : ℤ) (hL : XL ≡ YL [ZMOD R ^ (n + 1)])
       (hRight : XR ≡ YR [ZMOD R ^ (n + 1)]) :
       movingFrequencyGate v R T XL XR ↔ movingFrequencyGate w R T YL YR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFrequencyGate