ReducedCoefficientLift.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Using the remaining precision of reconstructed pivots in later coefficients

def OAI.Ostmann.liftResidueRepresentative line 14
Source documentation
An arbitrary representative at the original modulus. Its reduction is independent of this lift whenever the remaining precision suffices.
```
def liftResidueRepresentative (Q M : ℕ) (x : ZMod M) : ZMod Q := x.val
```
theorem OAI.Ostmann.reduce_liftResidueRepresentative line 16
theorem OAI.Ostmann.reduce_liftResidueRepresentative_int line 23

theorem OAI.Ostmann.reduce_ancestor_product line 30

Source documentation

A known nonbulk coefficient can include any specified finite set of ancestor pivots. Multiplication loses no further frequency precision.

theorem reduce_ancestor_product {I : Type*} [Fintype I]
    (Q M d : ℕ) [NeZero M] (hdQ : d ∣ Q) (hdM : d ∣ M)
    (C : ℤ) (x : I → ZMod M) (a : I → ℤ) (hx : ∀ i, x i = a i) :
    ZMod.castHom hdQ (ZMod d)
      ((C : ZMod Q) * ∏ i, liftResidueRepresentative Q M (x i)) =
      ((C * ∏ i, a i : ℤ) : ZMod d) := by
…

Mentions: OAI.Ostmann.liftResidueRepresentative

theorem OAI.Ostmann.frequency_dvd_remaining_precision line 45
Source documentation
After at most k divisions, the remaining R-power still contains each frequency divisor, so lifted ancestor coefficients can be tested modulo it.
```
theorem frequency_dvd_remaining_precision (R s k depth : ℕ)
    (hs : s ∣ R) (hdepth : depth ≤ k + 1) : s ∣ R ^ (k + 2 - depth) := by
…
```