OAI/NumberTheory/Ostmann/Construction/ModularAdaptiveCoefficients.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.SampledPivotHistory.modularValid line 12
2. def OAI.Ostmann.modularAdaptiveCoefficients line 21

   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 modularAdaptiveCoefficients (n R k : ℕ)
       (D : PivotDependencyScheme (2 ^ n - 1)) (U : Fin (2 ^ n - 1) → ℤ)
       (total : (ZMod (R ^ (k + 2)))ˣ) (past : List (ZMod (R ^ (k + 2)))ˣ) : ZMod (R ^ (k + 2)) × ZMod (R ^ (k + 2)) :=
   …

   Mentions: OAI.Ostmann.PivotDependencyScheme

3. theorem OAI.Ostmann.modularAdaptiveCoefficients_witness line 32
4. theorem OAI.Ostmann.modularAdaptiveCoefficients_reduce line 46

   Source documentation

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

   theorem modularAdaptiveCoefficients_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.modularValid D R k 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