OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternBulkKernel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_kernel_integral_comparison line 15

   Source documentation

   The sharp real kernel is constructed here. Compensation independence, all frequency bounds and both polynomial length budgets come from the actual pattern constructor, including its prescribed bulk permutation.

   theorem PublishedProgressionInput.movingPattern_kernel_integral_comparison
       (P : PublishedProgressionInput) {B C : Type*} {N n m r₀ : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (tierB : B → ℕ) (tierC : C → ℕ)
       (t : Bool → FrequencyTree ℤ n) (small : Bool → TreeLeafTuple (List B) n)
       (slot : (TreeLeafIndex n × Fin m) ↪ B) (perm : Equiv.Perm (TreeLeafIndex n × Fin m))
       (pattern : Bool × MovingSampleIndex n → C)
       (hB : ∀ i, n ≤ tierB i) (htier : ∀ i, tierC (pattern i) = movingSampleTier i.2)
       (hsmall : ∀ b, MovingLeafLengthLE n (small b) r₀)
       (base : Fin (N + 1) → ℝ) (childBound pivotBound : ℕ → ℕ)
       (j₀ : TreeLeafIndex n × Fin m)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi V : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (hfreq : ∀ b, ∀ s ∈ allFrequencyList n (t b), |(s : ℝ)| ≤ V)
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingSampleTier, OAI.Ostmann.MovingLeafLengthLE, OAI.Ostmann.allFrequencyList