OAI/NumberTheory/Ostmann/Arithmetic/MovingSampleDiagonalExpansion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.complexIntegerInterval_sum line 11
2. theorem OAI.Ostmann.complexIntegerInterval_const_mul line 19
3. theorem OAI.Ostmann.movingCompensatedAverage_diagonal_patterns line 31

   Source documentation

   The outer factor may contain the full cutoff weight and the common regular transform. It depends on the external draws, not the internal pair.

   theorem movingCompensatedAverage_diagonal_patterns {A : Type*} [Fintype A]
       (μ : ℕ → A → ℝ) (value : A → ℕ) (n : ℕ)
       (H K : ℝ → ℝ → MovingSampleSlots A n → ℂ)
       (W : ℝ → ℝ → ℂ) (u v r s center : ℝ) :
       letI := sampleSetoidFintype (Bool × MovingSampleIndex n)
   …

   Mentions: OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex