OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternLogKernelNormBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_log_norm_kernel_bound line 17

   Source documentation

   The original deleted prime kernel keeps its terminal log cutoffs. The main arithmetic norm bound is unchanged; only the explicit comparison error budget contains the additional logarithmic variation cost.

   theorem PublishedProgressionInput.movingPattern_log_norm_kernel_bound
       (P : PublishedProgressionInput) {B C Cell : Type*} [Fintype Cell]
       {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)
   …

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