MovingRegularMultiplierIdentity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The literal diagonal multiplier is the squared regular Fourier product

theorem OAI.Ostmann.movingRegularOther_eq_cofactor line 12
theorem OAI.Ostmann.naturalRegularMultiplier_eq_transform_norm line 24
theorem OAI.Ostmann.movingPattern_regular_multiplier_eq_transform line 43

theorem OAI.Ostmann.movingPattern_regular_multiplier_eq_primeProduct line 65

Source documentation

On the original support, the squared regular factor depends only on the prime product, frequency, outside product, and the two current giants.

theorem movingPattern_regular_multiplier_eq_primeProduct {B C : Type*} {N n m : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (t : Bool → FrequencyTree ℤ n)
    (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
    (pattern : Bool × MovingSampleIndex n → C) (value : Fin (N + 1) → ℕ)
    (hprime : ∀ i, (value i).Prime) (outside : List ℕ)
    (g : ∀ q : ℕ, ZMod q → ℂ) (s : ℤ) (XL XR : ℕ)
    (h : movingRegularOutsidePairwise value outside
      (movingPatternFinBulkData e n m t (fun _ => small) slot (Equiv.refl _) pattern false)) :
    let slots := movingPatternRegularSlots e n m small slot
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingRegularOutsidePairwise, OAI.Ostmann.movingPatternFinBulkData, OAI.Ostmann.movingPatternRegularSlots