MovingPatternPrimeRelabel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original pattern prime integral in the arithmetic coordinates

theorem OAI.Ostmann.movingPatternFinData_evaluate line 12

def OAI.Ostmann.movingPatternSupportedPrimeTerm line 28

Source documentation

The supported prime term of the original pattern, with its values pulled back along the finite assignment.

noncomputable def movingPatternSupportedPrimeTerm {σ I B C : Type}
    {N n : ℕ} (e : Fin (N + 1) ≃ B ⊕ C)
    (pattern : Bool × MovingSampleIndex n → C)
    (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
    (childBound pivotBound : ℕ → ℕ)
    (F : {d : ℕ} → MovingSlotData σ d → ℤ → ℂ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (t : Bool → FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List B) n)
    (x : Fin (N + 1) → σ) (b : Bool) (XL XR : ℕ) : ℂ :=
…

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

theorem OAI.Ostmann.movingOriginalPatternPrimeObservable_fin line 43