MovingWeightedMatchedMean.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original matched-history mean and its exact equality patterns

def OAI.Ostmann.movingWeightedMatchedKernel line 11

def OAI.Ostmann.movingWeightedMatchedMean line 31

Source documentation

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

noncomputable def movingWeightedMatchedMean {σ 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)
    (W : (B → σ) → ℝ → ℝ → ℂ) (u v r w center : ℝ) : ℂ :=
…

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

theorem OAI.Ostmann.movingWeightedMatchedMean_patterns line 49