OAI/NumberTheory/Ostmann/Arithmetic/MovingFourierSupported.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSlotWeight_leaf_support line 12

   Source documentation

   Every terminal factor of a nonzero recursive coefficient is nonzero. This statement keeps the concrete moving giant and terminal modulus.

   theorem movingSlotWeight_leaf_support {σ : Type*}
       (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ)
       (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (P : ℕ → ℤ → Prop)
       (hF : ∀ x s, F x s ≠ 0 → P (movingSlotModulus value x) s)
       {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
       (XL XR : ℕ)
       (hw : recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
         (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t ≠ 0) :
       ∀ i, P (T.leafModuli value XL XR i) (T.leafFrequencies i) := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.movingSlotModulus, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff

2. def OAI.Ostmann.movingWindowLeaf line 63
3. theorem OAI.Ostmann.moving_windowed_fourier_polynomial line 69

   Source documentation

   The original sharp terminal windows suffice for the clipped polynomial extension. All node and prime restrictions remain in the scalar coefficient.

   theorem moving_windowed_fourier_polynomial {σ : Type*}
       (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ)
       (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
       (hfreq : T.Frequencies (· ≠ 0)) (XL XR : ℕ) (L R : Polynomial ℝ) (z : ℝ)
       (hL : L.eval z = (XL : ℝ)) (hR : R.eval z = (XR : ℝ)) :
       recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
           (fun x s => movingWindowLeaf value X lo hi F x s * movingFourierLeaf value ψ X x s)
           (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t =
         recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingWindowLeaf, OAI.Ostmann.movingFourierLeaf, OAI.Ostmann.movingSlotCutoff