FullWeightFrequencies.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Nonzero frequencies from the actual unit and modulus-window support

theorem OAI.Ostmann.fullAtomTransferWeight_all_frequencies_ne_zero line 11

theorem OAI.Ostmann.fullAtomFourierWeight_zero_frequency line 47

Source documentation

A zero bottom frequency would make every atom equal to one. The actual initial modulus window excludes that case, including at its endpoints.

theorem fullAtomFourierWeight_zero_frequency {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
    (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hX : 0 < X) (hlo : 1 < X * lo)
    (x : CopyScheduleAtoms role 0 → ℕ) :
    fullAtomTransferWeight role childBound pivotBound ranges
      (fun τ v => (if (scheduleAtomTotal role τ : ℝ) / X ∈ Set.Icc lo hi then (1 : ℂ) else 0) *
        normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) v ((scheduleAtomTotal role τ : ℝ) / X))
      0 x (0 : ℤ) = 0 := by
…

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

theorem OAI.Ostmann.fullAtomFourierWeight_all_frequencies_ne_zero line 72