OAI/NumberTheory/Ostmann/Construction/WordHistoryCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.reconstructedWordFormula_realValue line 12
2. def OAI.Ostmann.HistoryCoefficientData.ofWords line 19
3. theorem OAI.Ostmann.HistoryCoefficientData.ofWords_complexity line 42
4. theorem OAI.Ostmann.HistoryCoefficientData.ofWords_value line 75

   Source documentation

   On the exact integral support, all Fourier and bin arguments are the original products after the specified prefix of pivot substitutions.

   theorem HistoryCoefficientData.ofWords_value {σ : Type*} {n t : ℕ}
       (steps : List (HistoryPivotStep σ)) (units : Fin steps.length → ℕ)
       (leafStage : Fin n → ℕ) (leafWord : Fin n → List σ)
       (rangeStage : Fin t → ℕ) (rangeWord : Fin t → List σ)
       (X : Fin n → ℝ) (ψ : 𝓢(ℝ, ℂ)) (v lo hi : Fin n → ℝ)
       (hlo : ∀ j, 1 ≤ lo j) (hhi : ∀ j, lo j ≤ hi j) (glo ghi : Fin t → ℝ)
       (x : σ → ℤ) (hx : ValidIntegerReconstruction steps x) :
       (HistoryCoefficientData.ofWords steps units leafStage leafWord rangeStage rangeWord
         X ψ v lo hi hlo hhi glo ghi).value x =
         (if ∀ i, IsUnit ((reconstructedPivotAt steps x i : ℤ) : ZMod (units i)) then 1 else 0) *
         (if (∀ j, ((((rangeWord j).map (reconstructIntegers (steps.take (rangeStage j)) x)).prod : ℤ) : ℝ)
             ∈ Set.Icc (glo j) (ghi j)) ∧
   …

   Mentions: OAI.Ostmann.HistoryPivotStep, OAI.Ostmann.ValidIntegerReconstruction, OAI.Ostmann.HistoryCoefficientData.ofWords, OAI.Ostmann.HistoryCoefficientData.value, OAI.Ostmann.reconstructedPivotAt, OAI.Ostmann.reconstructIntegers