OAI/NumberTheory/Ostmann/Arithmetic/GlobalHistoryCoefficient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.HistoryFormula.realValue line 11
2. theorem OAI.Ostmann.formulaPolynomial_eval_update line 15
3. theorem OAI.Ostmann.formulaFourier_polynomial_eval line 27
4. def OAI.Ostmann.globalHistoryArchCoefficient line 39
5. theorem OAI.Ostmann.globalHistoryArchCoefficient_local line 47
6. def OAI.Ostmann.globalHistoryCoefficient line 61
7. theorem OAI.Ostmann.globalHistoryCoefficient_local line 72

   Source documentation

   No support representation is assumed here: the global coefficient is identical to the polynomial coefficient used by the one-sided estimate.

   theorem globalHistoryCoefficient_local {σ : Type*} {n t : ℕ}
       (steps : List (HistoryPivotStep σ)) (units : Fin steps.length → ℕ)
       (F : Fin n → HistoryFormula σ) (G : Fin t → HistoryFormula σ)
       (X : Fin n → ℝ) (ψ : 𝓢(ℝ, ℂ)) (v lo hi : Fin n → ℝ)
       (hlo : ∀ j, 1 ≤ lo j) (hhi : ∀ j, lo j ≤ hi j) (glo ghi : Fin t → ℝ)
       (a : σ → ℤ) (coord : σ) (z : ℤ) :
       globalHistoryCoefficient steps units F G X ψ v lo hi glo ghi (Function.update a coord z) =
         reconstructedHistoryAmplitude steps units a coord
           (formulaFourierFactors F (fun j => (a j : ℝ)) coord X ψ v lo hi hlo hhi)
           (fullHistoryPolynomials (formulaFourierFactors F (fun j => (a j : ℝ)) coord X ψ v lo hi hlo hhi)
             (formulaRangePolynomials G (fun j => (a j : ℝ)) coord glo ghi))
           (fullHistoryKeep (polynomialRangeKeep t)) z := by
   …

   Mentions: OAI.Ostmann.HistoryPivotStep, OAI.Ostmann.HistoryFormula, OAI.Ostmann.globalHistoryCoefficient, OAI.Ostmann.reconstructedHistoryAmplitude, OAI.Ostmann.formulaFourierFactors, OAI.Ostmann.fullHistoryPolynomials, OAI.Ostmann.formulaRangePolynomials, OAI.Ostmann.fullHistoryKeep, OAI.Ostmann.polynomialRangeKeep