FullAtomFourierEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Energy of the actual Fourier weight from its initial modulus window

theorem OAI.Ostmann.normalizedFourier_window_square_exp_le line 11

theorem OAI.Ostmann.fullAtomFourierWeight_square_exp_le line 32

Source documentation

Every inherited support test is retained; the energy exponent comes solely from the initial product window and the Fourier transform's Schwartz seminorm.

theorem fullAtomFourierWeight_square_exp_le {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
    (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi Δ C K : ℝ) (hX : 0 < X)
    (hlo : Real.exp (Δ - C) ≤ lo)
    (hψ : SchwartzMap.seminorm ℝ 0 0 (𝓕 ψ : 𝓢(ℝ, ℂ)) ≤ Real.exp K)
    (n : ℕ) (x : CopyScheduleAtoms role n → ℕ) (t : FrequencyTree ℤ n) :
    ‖fullAtomTransferWeight role childBound pivotBound ranges
        (fun τ v => (if (scheduleAtomTotal role τ : ℝ) / X ∈ Set.Icc lo hi then (1 : ℂ) else 0) *
          normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) v ((scheduleAtomTotal role τ : ℝ) / X))
        n x t‖ ^ 2 ≤
      Real.exp (-(2 ^ n : ℕ) * Δ + (2 ^ n : ℕ) * (C + 2 * K)) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.scheduleAtomTotal, OAI.Ostmann.normalizedFourierProfile

theorem OAI.Ostmann.groupedFullCoprimeFourierWeight_square_exp_le line 49