OAI/NumberTheory/Ostmann/Arithmetic/MovingScalarWindows.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingDataLeaf line 11
2. def OAI.Ostmann.movingDataExtra line 15
3. def OAI.Ostmann.movingDataWeight line 19
4. theorem OAI.Ostmann.movingUnrestrictedWeight_data line 28
5. theorem OAI.Ostmann.movingUnrestrictedWeight_data_window line 41

   Source documentation

   Sharp terminal windows leave one fixed scalar coefficient. The test is on the actual terminal moduli obtained by the integer moving recursion.

   theorem movingUnrestrictedWeight_data_window {σ : Type*} (value : σ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       (X lo hi : ℝ) {n : ℕ} (T : MovingSlotData σ n) (XL XR : ℕ) :
       movingUnrestrictedWeight value (movingWindowLeaf value X lo hi (movingDataLeaf F))
           (movingDataExtra E) T XL XR =
         if ∀ i, (T.leafModuli value XL XR i : ℝ) / X ∈ Set.Icc lo hi
         then movingDataWeight F E T else 0 := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingUnrestrictedWeight, OAI.Ostmann.movingWindowLeaf, OAI.Ostmann.movingDataLeaf, OAI.Ostmann.movingDataExtra, OAI.Ostmann.movingDataWeight