OAI/NumberTheory/Ostmann/Arithmetic/MovingGiantFormulas.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotReversal.giantFormula line 10
2. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_value line 23

   Source documentation

   A supported integer reconstruction evaluates the rational giant formula exactly. The sampled compensation product appears in its denominator.

   theorem MovingSlotReversal.giantFormula_value {σ : Type*}
       (step : MovingSlotReversal σ) (value : σ → ℕ)
       (hs : step.rootFrequency ≠ 0)
       (hu : MovingSlotReversal.naturalProduct value step.compensationSlots ≠ 0)
       (L R : HistoryFormula Bool) (a : Bool → ℤ) (XL XR : ℕ)
       (hL : L.value (fun b => (a b : ℚ)) = (XL : ℚ))
       (hR : R.value (fun b => (a b : ℚ)) = (XR : ℚ))
       (hI : step.IntegralAt value (XL, XR)) :
       (step.giantFormula value hs hu L R).value (fun b => (a b : ℚ)) =
         (step.naturalPivot value XL XR : ℚ) := by
   …

   Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.HistoryFormula

3. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_integral line 40
4. theorem OAI.Ostmann.rational_nat_div_integral_iff line 54

   Source documentation

   The extra division by u is represented by an integer-polynomial residue test. It is not discarded when the ordinary transfer guards are idealized.

   theorem rational_nat_div_integral_iff (P u : ℕ) (hu : u ≠ 0) :
       (∃ z : ℤ, (P : ℚ) / u = (z : ℚ)) ↔ u ∣ P := by
   …