OAI/NumberTheory/Ostmann/Arithmetic/IndexedHistoryReconstruction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.reconstructionFormulaAt line 12
2. def OAI.Ostmann.reconstructedPivotAt line 19
3. theorem OAI.Ostmann.reconstructionFormulaAt_mem line 25
4. theorem OAI.Ostmann.mem_reconstructionTests_iff line 36
5. theorem OAI.Ostmann.reconstructionFormulaAt_value line 51
6. theorem OAI.Ostmann.smallDivisionTest_of_integer_value line 75
7. theorem OAI.Ostmann.reconstruction_small_tests_iff line 85

   Source documentation

   The entire original sequence of integrality and selected frequency-unit conditions equals the finite family of cleared polynomial residue tests.

   theorem reconstruction_small_tests_iff {σ : Type*} (steps : List (HistoryPivotStep σ))
       (x : σ → ℤ) (s : Fin steps.length → ℕ) :
       (∀ i, smallDivisionTest
         (MvPolynomial.eval₂Hom (RingHom.id ℤ) x
           (reconstructionFormulaAt steps HistoryFormula.prime i).cleared.numerator)
         (reconstructionFormulaAt steps HistoryFormula.prime i).cleared.denominator (s i)) ↔
       ValidIntegerReconstruction steps x ∧
         ∀ i, IsUnit ((reconstructedPivotAt steps x i : ℤ) : ZMod (s i)) := by
   …

   Mentions: OAI.Ostmann.HistoryPivotStep, OAI.Ostmann.smallDivisionTest, OAI.Ostmann.reconstructionFormulaAt, OAI.Ostmann.ValidIntegerReconstruction, OAI.Ostmann.reconstructedPivotAt