OAI/NumberTheory/Ostmann/Arithmetic/MovingOriginalDiagonalMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingExternalDiagonalWeight line 14

   Source documentation

   The common regular multiplier depends only on the external draws.

   noncomputable def movingExternalDiagonalWeight {σ B : Type*} {n : ℕ}
       (value : σ → ℕ) (outside : List ℕ) (small bulk : TreeLeafTuple (List B) n)
       (greg : ∀ q : ℕ, ZMod q → ℂ) (sreg : ℤ)
       (φ : ℝ → ℝ) (Jleft Jright : ℝ) (diagonal : Bool)
       (y : B → σ) (x z : ℝ) : ℂ :=
   …

   Mentions: OAI.Ostmann.TreeLeafTuple

2. def OAI.Ostmann.movingOriginalDiagonalKernel line 26
3. def OAI.Ostmann.movingOriginalDiagonalMean line 47

   Source documentation

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

   noncomputable def movingOriginalDiagonalMean {σ 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)
       (greg : ∀ q : ℕ, ZMod q → ℂ) (sreg : ℤ)
       (Jleft Jright : ℝ) (diagonal : Bool) (u v r w center : ℝ) : ℂ :=
   …

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

4. theorem OAI.Ostmann.movingOriginalDiagonalMean_patterns line 66