OAI/NumberTheory/Ostmann/Arithmetic/RealNodeSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotReversal.realCompositePivot line 11
2. def OAI.Ostmann.realValueNodeSupport line 16
3. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_realEval line 29
4. theorem OAI.Ostmann.movingNodeGuard_realEval line 40
5. theorem OAI.Ostmann.realValueNodeSupport_nat line 54

   Source documentation

   Exact agreement with all original archimedean formula-node tests.

   theorem realValueNodeSupport_nat {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0))
       (L R : HistoryFormula Bool) (x : Bool → ℝ) :
       movingArchimedeanGate (T.formulaNodes value hvalue childBound pivotBound hf L R) x ↔
         realValueNodeSupport (fun i => (value i : ℝ)) childBound pivotBound T (L.realEval x) (R.realEval x) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.HistoryFormula, OAI.Ostmann.movingArchimedeanGate, OAI.Ostmann.realValueNodeSupport