OAI/NumberTheory/Ostmann/Arithmetic/BulkFrequencyFactor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingFrequencyCore line 11
2. theorem OAI.Ostmann.movingFrequencyPairFactor_core line 22

   Source documentation

   The only nonperiodic part of this factor consists of the explicit regular-prime coincidence tests. The remaining node bounds are independent of the numerical bulk values.

   theorem movingFrequencyPairFactor_core {σ : Type*} (value : σ → ℕ)
       (outside : List ℕ)
       (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       {n : ℕ} (T : Bool → MovingSlotData σ n) (nodes : Bool → List MovingFormulaNode)
       (R x y : ℤ) :
       movingFrequencyPairFactor value outside F E T nodes R x y =
         (if ∀ b, movingRegularOutsidePairwise value outside (T b) ∧
           (∀ f ∈ nodes b, f.guard.frequencyBounds) then (1 : ℂ) else 0) *
         movingFrequencyCore value F E T R x y := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.movingFrequencyPairFactor, OAI.Ostmann.movingRegularOutsidePairwise, OAI.Ostmann.movingFrequencyCore

3. theorem OAI.Ostmann.movingFrequencyCore_values_modEq line 49

   Source documentation

   Unlike the removed coincidence tests, the actual frequency core is constant on the joint bulk residue cells.

   theorem movingFrequencyCore_values_modEq {σ : Type*} (v w : σ → ℕ)
       (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       {n : ℕ} (T : Bool → MovingSlotData σ n) (R : ℤ)
       (hf : ∀ b, (T b).Frequencies (· ≠ 0))
       (hcomp : ∀ b, (T b).CompensationAgreement v w)
       (hR : ∀ b, (T b).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)]) :
       movingFrequencyCore v F E T R XL XR = movingFrequencyCore w F E T R YL YR := by
   …

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

4. def OAI.Ostmann.MovingSlotData.FrequencyBounds line 66
5. theorem OAI.Ostmann.MovingSlotData.formulaNodes_frequencyBounds line 74