OAI/NumberTheory/Ostmann/Arithmetic/MovingReducedPageAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingReducedPair_regular_page_average line 13

   Source documentation

   All non-Page hypotheses here are the actual small-slot and tree data. The periodicity and regular-block coprimality are derived from those data.

   theorem movingReducedPair_regular_page_average {σ I J : Type*} [Fintype J] [DecidableEq J]
       (P : PublishedProgressionInput) (N : ℕ) (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
       (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
       (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : Bool → ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       {n : ℕ} (T : Bool → MovingSlotData σ n) (hf : ∀ b, (T b).Frequencies (· ≠ 0))
       (hlevels : ∀ b, (T b).Levels tier)
       (hsmall : ∀ b i, (T b).Frequencies (fun s => IsCoprime s (value i : ℤ)))
       (hout : ∀ b, movingRegularOutsidePairwise value outside (T b))
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingRegularOutsidePairwise