OAI/NumberTheory/Ostmann/Arithmetic/MovingFullSmooth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_full_smooth_polynomial line 14

   Source documentation

   Every original logarithmic node cutoff and normalized Fourier leaf is represented by the one constructed polynomial family. Arithmetic restrictions and compensation powers stay in the original scalar coefficient.

   theorem moving_full_smooth_polynomial {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ) (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0)
       {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)
   …

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

2. theorem OAI.Ostmann.moving_full_smooth_spectator_decomposition line 50

   Source documentation

   The complete moving coefficient splits into the original scalar support, its actual smooth polynomial weight, and all of its spectator trees. No nonzero-term hypothesis is needed.

   theorem moving_full_smooth_spectator_decomposition {σ I : Type*}
       (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ) (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (hextra : ∀ i x s v w, extra x s v w ≠ 0 →
         (historyPivot (movingSlotSystem value childBound pivotBound) x s v w : ZMod (q i)) ≠ 0)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0)
       {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.historyPivot, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree