AdaptivePivotCoefficients.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Constructing coefficients from the already exposed product prefix

structure OAI.Ostmann.SampledPivotHistory line 14
Source documentation
Actual integer products together with their exact unit residues.
```
structure SampledPivotHistory (n Q : ℕ) where
…
```
def OAI.Ostmann.SampledPivotHistory.leftProduct line 20
def OAI.Ostmann.SampledPivotHistory.rightProduct line 23
def OAI.Ostmann.SampledPivotHistory.valid line 26
def OAI.Ostmann.SampledPivotHistory.matches line 32
def OAI.Ostmann.adaptivePivotCoefficients line 39
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 adaptivePivotCoefficients (n Q : ℕ)
    (D : PivotDependencyScheme (2 ^ n - 1))
    (total : (ZMod Q)ˣ) (past : List (ZMod Q)ˣ) : ZMod Q × ZMod Q :=
…
```
Mentions: OAI.Ostmann.PivotDependencyScheme
theorem OAI.Ostmann.adaptivePivotCoefficients_witness line 50

theorem OAI.Ostmann.SampledPivotHistory.prefix_products line 64

Source documentation

Two completions of one prefix agree on the bulk products at every previously exposed node.

theorem SampledPivotHistory.prefix_products {n Q : ℕ}
    (a b : SampledPivotHistory n Q) (total : (ZMod Q)ˣ) (past : List (ZMod Q)ˣ)
    (ha : a.matches total past) (hb : b.matches total past)
    (hj : past.length ≤ 2 ^ n - 1) (i : Fin (2 ^ n - 1)) (hi : i.val < past.length) :
    (a.leftProduct i : ZMod Q) = b.leftProduct i ∧
      (a.rightProduct i : ZMod Q) = b.rightProduct i := by
…

Mentions: OAI.Ostmann.SampledPivotHistory

theorem OAI.Ostmann.adaptivePivotCoefficients_reduce line 83

Source documentation

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

theorem adaptivePivotCoefficients_reduce (n R k : ℕ)
    (D : PivotDependencyScheme (2 ^ n - 1))
    (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.valid D)
    (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