OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternBulkLog.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.selectedBulkSet line 13
2. theorem OAI.Ostmann.mem_selectedBulkSet line 16
3. theorem OAI.Ostmann.selectedBulkLogValues line 20
4. theorem OAI.Ostmann.selectedBulkLogValues_nat line 33
5. theorem OAI.Ostmann.movingPatternBulkSet_compensationAbsent line 46
6. theorem OAI.Ostmann.movingPattern_bulk_kernel_nat line 60

   Source documentation

   At original prime tuples the real extension has exactly the original sharp gates and Fourier windows. This includes every boundary point.

   theorem movingPattern_bulk_kernel_nat {B C : Type*} {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ 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)
       (base value : Fin (N + 1) → ℕ)
       (hv : ∀ i ∉ Set.range (movingPatternBulkEmbedding e slot), value i = base i)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       (hf : ∀ b, ∀ s ∈ allFrequencyList n (t b), s ≠ 0)
       (ψ : SchwartzMap ℝ ℂ) (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (L R : ℝ) :
       let T := movingPatternFinBulkData e n m t small slot perm pattern
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternBulkEmbedding, OAI.Ostmann.allFrequencyList, OAI.Ostmann.movingPatternFinBulkData