OAI/NumberTheory/Ostmann/Arithmetic/ReconstructedHistoryTests.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.ClearedHistoryValue.real_value_of_integer line 14

   Source documentation

   Cast the exact integral numerator equation, avoiding any approximation of a reconstructed rational value.

   theorem ClearedHistoryValue.real_value_of_integer {σ : Type*} (F : ClearedHistoryValue σ)
       (x : σ → ℤ) (y : ℤ) (hy : F.eval (fun i => (x i : ℚ)) = y) :
       MvPolynomial.eval₂ (Int.castRingHom ℝ) (fun i => (x i : ℝ)) F.numerator /
         (F.denominator : ℝ) = y := by
   …

   Mentions: OAI.Ostmann.ClearedHistoryValue

2. theorem OAI.Ostmann.reconstructed_integer_coprimality line 29
3. theorem OAI.Ostmann.reconstructed_integer_real line 39
4. theorem OAI.Ostmann.reconstructed_integer_range line 50

   Source documentation

   Every retained pivot or product range is exactly a pair of polynomial inequalities after fixing all but one of the original independent primes.

   theorem reconstructed_integer_range {σ : Type*} (steps : List (HistoryPivotStep σ))
       (x : σ → ℤ) (i coord : σ) (lo hi : ℝ) (z : ℤ)
       (hx : ValidIntegerReconstruction steps (Function.update x coord z)) :
       clearedIntervalKeep (polynomialSupportCode
         (clearedIntervalPolynomials
           (specializeHistoryVariable (fun j => (x j : ℝ)) coord
             (integerReconstructionFormulas steps i).cleared.numerator)
           ((integerReconstructionFormulas steps i).cleared.denominator : ℝ) lo hi) z) = true ↔
         (reconstructIntegers steps (Function.update x coord z) i : ℝ) ∈ Set.Icc lo hi := by
   …

   Mentions: OAI.Ostmann.HistoryPivotStep, OAI.Ostmann.ValidIntegerReconstruction, OAI.Ostmann.clearedIntervalKeep, OAI.Ostmann.polynomialSupportCode, OAI.Ostmann.clearedIntervalPolynomials, OAI.Ostmann.specializeHistoryVariable, OAI.Ostmann.integerReconstructionFormulas, OAI.Ostmann.reconstructIntegers