OAI/NumberTheory/Ostmann/Construction/HistoryFormulaFourier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.formulaFourierFactors line 12
2. def OAI.Ostmann.formulaFourierBudget line 19
3. theorem OAI.Ostmann.formulaFourierFactors_budget line 23
4. theorem OAI.Ostmann.formulaFourierBudget_nonneg line 30
5. theorem OAI.Ostmann.formulaFourierFactors_degree line 38
6. theorem OAI.Ostmann.formulaFourier_full_complexity line 48

   Source documentation

   All critical points, Fourier ranges, and original word/pivot ranges have a polynomial complexity obtained from the actual formula costs.

   theorem formulaFourier_full_complexity {σ : Type*} {n t : ℕ}
       (F : Fin n → HistoryFormula σ) (G : Fin t → HistoryFormula σ)
       (a : σ → ℝ) (coord : σ) (X : Fin n → ℝ) (ψ : 𝓢(ℝ, ℂ))
       (v lo hi : Fin n → ℝ) (hlo : ∀ j, 1 ≤ lo j) (hhi : ∀ j, lo j ≤ hi j)
       (glo ghi : Fin t → ℝ) :
       let factors := formulaFourierFactors F a coord X ψ v lo hi hlo hhi
   …

   Mentions: OAI.Ostmann.HistoryFormula, OAI.Ostmann.formulaFourierFactors

7. theorem OAI.Ostmann.formulaFourierFactor_integer_value line 63