MovingPatternMainGain.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual quartet main term absorbs the full sharp kernel cost

theorem OAI.Ostmann.exists_movingPatternMainGain line 14

Source documentation

A single mixed-character tolerance and prime threshold work for all actual pattern trees and bulk lengths. No local cancellation bound is an assumption here: it is derived from the quartet theorem.

theorem exists_movingPatternMainGain (ψ : 𝓢(ℝ, ℂ)) (n r₀ : ℕ)
    (A lo hi B D F gain : ℝ) (hA : 0 ≤ A) (hhi : lo ≤ hi) :
    ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧ ∃ cutoff : ℕ, 3 ≤ cutoff ∧
      ∀ (m : ℕ), 1 ≤ m → ∀ (Bidx Cidx : Type) (N : ℕ)
        (e : Fin (N + 1) ≃ Bidx ⊕ Cidx) (base : Fin (N + 1) → ℕ)
        (t : Bool → FrequencyTree ℤ (n + 2))
        (small : Bool → TreeLeafTuple (List Bidx) (n + 2))
        (pattern : Bool × MovingSampleIndex (n + 2) → Cidx)
        (p : Fin m → ℕ) [∀ i, Fact (p i).Prime],
      (∀ i, cutoff ≤ p i) →
      (∀ i b, ∀ s ∈ allFrequencyList (n + 2) (t b), s ≠ 0 ∧ s.natAbs < p i) →
      (∀ i b, ∀ j ∈ flattenMovingSlots (n + 2) (small b),
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.allFrequencyList, OAI.Ostmann.flattenMovingSlots