OAI/NumberTheory/Ostmann/Arithmetic/MovingOriginalPrimeExpansion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingOriginalSampleAverage_compensated line 10
2. theorem OAI.Ostmann.movingOriginal_prime_pair_patterns line 32

   Source documentation

   The finite original giant-prime square is exactly a sum of pattern means of the original fully supported history pair. This is the input to the proved prime-to-Page comparison; no prime is removed or reweighted here.

   theorem movingOriginal_prime_pair_patterns {σ I : Type*} [Fintype σ]
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (μ : ℕ → σ → ℝ) (childBound pivotBound : ℕ → ℕ)
       (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : Bool → ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (t : Bool → FrequencyTree ℤ n) (small bulk : Bool → TreeLeafTuple (List σ) n)
       (u v r s : ℝ) :
       letI := sampleSetoidFintype (Bool × MovingSampleIndex n)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex