OAI/NumberTheory/Ostmann/Arithmetic/MovingRealResidues.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.HistoryFormula.realEval line 10
2. def OAI.Ostmann.WordTransferGuard.archimedeanAt line 13
3. theorem OAI.Ostmann.WordTransferGuard.validAt_residue_archimedean line 20

   Source documentation

   Integrality turns the strict integer gap into the closed real inequality. All divisibility and unit tests remain in the residue factor.

   theorem WordTransferGuard.validAt_residue_archimedean {σ : Type*}
       (g : WordTransferGuard σ) (x : σ → ℤ) :
       g.ValidAt x ↔ g.residueAt x ∧ g.frequencyBounds ∧
         g.archimedeanAt (fun i => (x i : ℝ)) := by
   …

   Mentions: OAI.Ostmann.WordTransferGuard

4. theorem OAI.Ostmann.MovingFormulaNode.holds_residue_archimedean line 33
5. def OAI.Ostmann.movingResidueGate line 40
6. def OAI.Ostmann.movingArchimedeanGate line 43
7. theorem OAI.Ostmann.movingFormulaNodes_residue_real line 48

   Source documentation

   The real factor is evaluated at the actual point, while the residue factor may use any representative of the constructed common period.

   theorem movingFormulaNodes_residue_real (nodes : List MovingFormulaNode)
       (x a : Bool → ℤ) (hres : ∀ i, x i ≡ a i [ZMOD movingArithmeticPeriod nodes]) :
       (∀ f ∈ nodes, f.guard.ValidAt x ∧ f.newGiant.IntegralAt x) ↔
         movingResidueGate nodes a ∧ movingArchimedeanGate nodes (fun i => (x i : ℝ)) := by
   …

   Mentions: OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.movingArithmeticPeriod, OAI.Ostmann.movingResidueGate, OAI.Ostmann.movingArchimedeanGate

8. def OAI.Ostmann.topGiantReal line 67
9. def OAI.Ostmann.WordTransferGuard.realPolynomials line 69
10. theorem OAI.Ostmann.WordTransferGuard.archimedeanAt_polynomials line 76
11. theorem OAI.Ostmann.WordTransferGuard.realPolynomials_degree line 85
12. def OAI.Ostmann.movingArchimedeanRootCuts line 99
13. def OAI.Ostmann.movingRealUpdate line 103
14. theorem OAI.Ostmann.movingArchimedeanRootCuts_mem line 106
15. theorem OAI.Ostmann.movingArchimedeanGate_rootCell line 113
16. theorem OAI.Ostmann.movingArithmeticSupport_residue_real line 130