MovingOriginalMatchedMean.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original matched-history mean and its exact equality patterns

def OAI.Ostmann.movingOriginalMatchedKernel line 11

def OAI.Ostmann.movingOriginalMatchedMean line 32

Source documentation

Both history averages and the external law are the original ones.

noncomputable def movingOriginalMatchedMean {σ I B : Type*}
    [Fintype σ] [Fintype B] (q : I → ℕ) [∀ i, Fact (q i).Prime]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ) (ν : B → σ → ℝ)
    (childBound pivotBound : ℕ → ℕ) (f : ℤ → ℂ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (n : ℕ) (t : Bool → FrequencyTree ℤ n) (small : TreeLeafTuple (List B) n) (bulk : Bool → TreeLeafTuple (List B) n)
    (greg : ∀ q : ℕ, ZMod q → ℂ) (sreg : ℤ)
    (Jleft Jright : ℝ) (diagonal : Bool) (u v r w center : ℝ) : ℂ :=
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple

theorem OAI.Ostmann.movingOriginalMatchedMean_patterns line 51