OAI/NumberTheory/Ostmann/Arithmetic/MovingSignedFormulas.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.rational_int_div_integral_iff line 11
2. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_signed_value line 23
3. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_signed_integral_iff line 36
4. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_of_signed_integral line 54
5. theorem OAI.Ostmann.MovingSlotData.formulaNodes_signed_integral_iff line 69

   Source documentation

   The integrality entries of the original formula list impose exactly the signed divisions. They do not need any real or positivity hypothesis.

   theorem MovingSlotData.formulaNodes_signed_integral_iff {σ : Type*}
       (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
       (childBound pivotBound : ℕ → ℕ) {n : ℕ} (T : MovingSlotData σ n)
       (hf : T.Frequencies (· ≠ 0)) (L R : HistoryFormula Bool) (a : Bool → ℤ) (x y : ℤ)
       (hL : L.value (fun b => (a b : ℚ)) = (x : ℚ))
       (hR : R.value (fun b => (a b : ℚ)) = (y : ℚ)) :
       (∀ f ∈ T.formulaNodes value hvalue childBound pivotBound hf L R, f.newGiant.IntegralAt a) ↔
         T.SignedIntegral value x y := by
   …

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