OAI/NumberTheory/Ostmann/Construction/ScheduledFourierEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.clippedFullAtomFourierWeight line 12
2. theorem OAI.Ostmann.clippedFullAtomFourierWeight_square_le line 21
3. theorem OAI.Ostmann.scheduled_full_fourier_energy_le line 42

   Source documentation

   Extending the internal frequency sets costs no multiplicity. All original prime laws, bottom cutoffs and recursive support conditions remain in the sum.

   theorem scheduled_full_fourier_energy_le {I A : Type*} [Fintype I] [Fintype A]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hX : 0 < X) (hlo : 1 < X * lo)
       (V : ℕ → ℕ) (hV : Monotone V) (n : ℕ)
       (μ : A → ℝ) (hμ : ∀ q, 0 ≤ μ q) (values : A → CopyScheduleAtoms role n → ℕ) :
       (∑ a : ScheduledFrequencyIndex V n, ∑ q, μ q *
         ‖fullAtomTransferWeight role childBound pivotBound ranges (scheduleFourierLeaf role ψ X lo hi)
           n (values q) (scheduledFrequencyHistory V n a)‖ ^ 2) ≤
         ∑ t : FrequencyTree ((transferFrequencyRange (V n)).erase 0) n, ∑ q, μ q *
           ‖clippedFullAtomFourierWeight role childBound pivotBound ranges ψ X lo hi
             ((transferFrequencyRange (V n)).erase 0) (V 0) n (values q) t‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ScheduledFrequencyIndex, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.scheduleFourierLeaf, OAI.Ostmann.scheduledFrequencyHistory, OAI.Ostmann.FrequencyTree, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.clippedFullAtomFourierWeight