MovingFourierFactor.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial smooth factors in the full moving-giant coefficient

def OAI.Ostmann.movingFourierLeaf line 10
def OAI.Ostmann.movingFourierTree line 14
def OAI.Ostmann.movingPolynomialFourierTree line 23
theorem OAI.Ostmann.movingPolynomialFourierTree_eq line 34

theorem OAI.Ostmann.movingSlotWeight_fourier line 55

Source documentation

The exact Fourier factorization preserves all original support terms, including terms whose full coefficient is zero.

theorem movingSlotWeight_fourier {σ : Type*}
    (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ)
    (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (ψ : ℝ → ℂ) (X : ℝ) {n : ℕ}
    (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t) (XL XR : ℕ) :
    recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
        (fun x s => F x s * movingFourierLeaf value ψ X x s)
        (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t =
      recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
        (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t *
        movingFourierTree value ψ X T XL XR := by
…

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

theorem OAI.Ostmann.movingSlotWeight_polynomial_fourier line 99

Source documentation

The polynomial smooth extension agrees with the full coefficient on its proved integer support. No polynomial realization premise is required.

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