MovingWeightedDiagonalMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Equality patterns with a retained external Fourier multiplier

def OAI.Ostmann.movingWeightedDiagonalKernel line 13

def OAI.Ostmann.movingWeightedDiagonalMean line 33

Source documentation

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

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

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

theorem OAI.Ostmann.movingWeightedDiagonalMean_patterns line 51
theorem OAI.Ostmann.movingWeightedDiagonalMean_zero_frequency line 95