OAI/NumberTheory/Ostmann/Construction/CompensatedAdaptiveCoefficients.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.SampledPivotHistory.compensatedValid line 12
2. def OAI.Ostmann.compensatedAdaptiveCoefficients line 20

   Source documentation

   Choose any valid completion of the exposed prefix. The precision theorem below proves that the required reduced coefficients do not depend on it.

   noncomputable def compensatedAdaptiveCoefficients (n Q : ℕ)
       (D : PivotDependencyScheme (2 ^ n - 1)) (U : Fin (2 ^ n - 1) → ℤ)
       (total : (ZMod Q)ˣ) (past : List (ZMod Q)ˣ) : ZMod Q × ZMod Q :=
   …

   Mentions: OAI.Ostmann.PivotDependencyScheme

3. theorem OAI.Ostmann.compensatedAdaptiveCoefficients_witness line 31
4. theorem OAI.Ostmann.compensatedAdaptiveCoefficients_reduce line 45

   Source documentation

   The chosen completion gives the actual coefficients modulo the current root frequency, even though its integer pivots may differ.

   theorem compensatedAdaptiveCoefficients_reduce (n R k : ℕ)
       (D : PivotDependencyScheme (2 ^ n - 1)) (U : Fin (2 ^ n - 1) → ℤ)
       (hU : ∀ i, IsCoprime (U i) (R : ℤ))
       (hdepth : ∀ i, D.depth i ≤ k) (hs : ∀ i, (D.frequencies i).root ≠ 0)
       (hsR : ∀ i, (D.frequencies i).root.natAbs ∣ R)
       (a : SampledPivotHistory n (R ^ (k + 2))) (ha : a.compensatedValid D U)
       (total : (ZMod (R ^ (k + 2)))ˣ) (past : List (ZMod (R ^ (k + 2)))ˣ)
       (hm : a.matches total past) (hj : past.length < 2 ^ n - 1) :
       let j : Fin (2 ^ n - 1) := ⟨past.length, hj⟩
   …

   Mentions: OAI.Ostmann.PivotDependencyScheme, OAI.Ostmann.SampledPivotHistory