RecursiveArchimedeanCutoff.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The original Fourier weight retains its precise bottom cutoff

theorem OAI.Ostmann.recursive_archimedean_square_with_leaf_cutoff line 13

Source documentation

The original level-zero Fourier factor vanishes outside its prescribed frequency range; each recursive coefficient retains every leaf cutoff.

theorem recursive_archimedean_square_with_leaf_cutoff {State : Type*}
    (sys : TransferHistorySystem State) (M : State → ℕ) (c : State → ℤ → ℝ)
    (cutoff : State → ℤ → ℤ → ℤ → ℝ) (X Δ C K : ℝ) (ψhat : ℝ → ℂ)
    (hc : ∀ σ v, |c σ v| ≤ 1) (hψ : ∀ u, ‖ψhat u‖ ≤ Real.exp K)
    (hwindow : ∀ σ v, c σ v ≠ 0 → 0 < M σ ∧ X * Real.exp (Δ - C) ≤ M σ)
    (hcut : ∀ σ s v w, |cutoff σ s v w| ≤ 1)
    (V : ℕ) (hfreq : ∀ σ v, c σ v ≠ 0 → v.natAbs ≤ V)
    (S : Finset ℤ) (n : ℕ) (σ : State) (t : FrequencyTree S n) :
    ‖recursiveTransferWeight sys
        (fun σ v => archimedeanLeafFactor X (M σ) v (c σ v) ψhat) cutoff n σ
        (frequencyTreeMap Subtype.val n t)‖ ^ 2 ≤
      Real.exp (-(2 ^ n : ℕ) * Δ + (2 ^ n : ℕ) * (C + 2 * K)) *
…

Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.archimedeanLeafFactor, OAI.Ostmann.frequencyTreeMap