MovingFullFourier.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The full supported coefficient with its explicit polynomial smooth part

theorem OAI.Ostmann.moving_full_fourier_decomposition line 15

Source documentation

The actual full integrand separates into its original support coefficient, the constructed Fourier polynomials, and the actual moving spectator trees. This includes every zero-support term.

theorem moving_full_fourier_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) → ℂ) (D : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (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 : ℝ)) :
…

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