MovingOriginalEnergyPatterns.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual coefficient energy as a sum over the original equality patterns

theorem OAI.Ostmann.movingFrequencyCoefficient_original_pattern_bound line 13

Source documentation

The original coefficient square is bounded by the absolute pattern means with both histories' bottom cutoffs retained. There is no extra root-frequency or ambient-prime cardinality factor.

theorem movingFrequencyCoefficient_original_pattern_bound {σ I B : Type}
    [Fintype σ] [Fintype B]
    (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
    (μ : ℕ → σ → ℝ) (ν : B → σ → ℝ) (childBound pivotBound V : ℕ → ℕ)
    (F : {d : ℕ} → MovingSlotData σ d → ℤ → ℂ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (n : ℕ) (small bulk : TreeLeafTuple (List B) n) (u v r w : ℝ)
    (hV : Monotone V) (hF : ∀ d (T : MovingSlotData σ d), F T 0 = 0)
    (N : Setoid (Bool × MovingSampleIndex n) → ℕ)
    (e : ∀ s : Setoid (Bool × MovingSampleIndex n), Fin (N s + 1) ≃ B ⊕ Quotient s) :
    let _ := sampleSetoidFintype (Bool × MovingSampleIndex n)
…

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