OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternLogSeparatedBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The actual pattern kernel, frequency factor and spectator factors can be averaged under the original deleted prime law. The comparison error here is derived from the published progression input, with the concrete tree degrees; the sharp kernel and the old prime normalizers are retained.

   theorem PublishedProgressionInput.movingPattern_log_separated_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