OAI/NumberTheory/Ostmann/Construction/HistoryFourierPolynomial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.historyFourierFactor line 12
2. theorem OAI.Ostmann.historyFourierFactor_value line 19

   Source documentation

   This is the actual level-zero Fourier weight after fixing the other variables and substituting the cleared history numerator.

   theorem historyFourierFactor_value {σ : Type*} (P : MvPolynomial σ ℤ)
       (a : σ → ℝ) (i : σ) (d X : ℝ) (ψ : 𝓢(ℝ, ℂ))
       (v lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (x : ℝ)
       (hd : d ≠ 0) (hX : X ≠ 0)
       (hP : MvPolynomial.eval₂ (Int.castRingHom ℝ) (Function.update a i x) P ≠ 0)
       (hrange : (MvPolynomial.eval₂ (Int.castRingHom ℝ) (Function.update a i x) P / d) / X ∈
         Set.Icc lo hi) :
       (historyFourierFactor P a i d X ψ v lo hi hlo hhi).value x =
         archimedeanLeafFactor X
           (MvPolynomial.eval₂ (Int.castRingHom ℝ) (Function.update a i x) P / d) v 1 ψ := by
   …

   Mentions: OAI.Ostmann.historyFourierFactor, OAI.Ostmann.archimedeanLeafFactor

3. theorem OAI.Ostmann.historyFourierFactor_degree line 35
4. theorem OAI.Ostmann.historyFourierFactor_budget line 43