MovingPatternPrimeIntegralBridge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The original prime integrand and the integrated pattern CRT identity

theorem OAI.Ostmann.movingOriginalPatternPrimeObservable_pair_frequency line 14

Source documentation

The leaf frequency mask has no dependence on the names of sampled slots.

theorem movingOriginalPatternPrimeObservable_pair_frequency {σ I B C : Type}
    {N n m : ℕ} (e : Fin (N + 1) ≃ B ⊕ C)
    (pattern : Bool × MovingSampleIndex n → C)
    (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
    (childBound pivotBound : ℕ → ℕ) (f : ℤ → ℂ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (t : Bool → FrequencyTree ℤ n) (small : TreeLeafTuple (List B) n)
    (slot : (TreeLeafIndex n × Fin m) ↪ B)
    (x : Fin (N + 1) → σ) (u v r s : ℝ) :
    movingOriginalPatternPrimeObservable e pattern q value outside childBound pivotBound
      (fun {_} _ => f) g Dq S ψ X lo hi φ G t small (bulkSlotLeaves n m slot) u v r s x =
…

Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.movingOriginalPatternPrimeObservable, OAI.Ostmann.bulkSlotLeaves

theorem OAI.Ostmann.movingPatternTwoPrimeObservable_integral_crt line 50