MovingSignedUnits.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The giant unit tests on signed residue representatives

theorem OAI.Ostmann.int_modEq_isCoprime_iff line 11

def OAI.Ostmann.MovingSlotData.frequencyProduct line 22

Source documentation

The product records every frequency at or below this state.

def MovingSlotData.frequencyProduct {σ : Type*} : {n : ℕ} → MovingSlotData σ n → ℤ
  | _, .leaf s _ => s
  | _, .node s _ _ _ left right => s * left.frequencyProduct * right.frequencyProduct

Mentions: OAI.Ostmann.MovingSlotData

theorem OAI.Ostmann.MovingSlotData.frequencies_isCoprime line 26
def OAI.Ostmann.movingLocalGiantUnits line 37
Source documentation
Tests the two giants against every subtree frequency, every current regular slot, and the fixed outside list. Mutual coprimality of the two current giants is deliberately separate.
```
def movingLocalGiantUnits {σ : Type*} (value : σ → ℕ) (outside : List ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (XL XR : ℤ) : Prop :=
…
```
Mentions: OAI.Ostmann.MovingSlotData

def OAI.Ostmann.movingSignedGiantUnits line 46

Source documentation

Signed evaluation uses exact Euclidean division and hence is defined on all residue representatives, including representatives off the real support.

noncomputable def movingSignedGiantUnits {σ : Type*} (value : σ → ℕ) (outside : List ℕ) :
    {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → Prop
  | _, T@(.leaf _ _), XL, XR => movingLocalGiantUnits value outside T XL XR
  | _, T@(.node s CL CR U left right), XL, XR =>
      let p := (MovingSlotData.step s CL CR U left right false).signedPivot value XL XR
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingLocalGiantUnits, OAI.Ostmann.MovingSlotData.step

def OAI.Ostmann.movingNaturalGiantUnits line 55
theorem OAI.Ostmann.movingSignedGiantUnits_nat line 64

def OAI.Ostmann.movingGiantUnitPeriod line 77

Source documentation

A period for precisely the current unit tests and their descendant Euclidean divisions. No real inequalities are used in this definition.

def movingGiantUnitPeriod {σ : Type*} (value : σ → ℕ) (outside : List ℕ) :
    {n : ℕ} → MovingSlotData σ n → ℤ
  | _, T@(.leaf _ _) =>
      T.frequencyProduct * (MovingSlotReversal.naturalProduct value T.regularSlots : ℤ) * outside.prod
  | _, T@(.node s _ _ U left right) =>
      (T.frequencyProduct * (MovingSlotReversal.naturalProduct value T.regularSlots : ℤ) * outside.prod) *
        (s * (MovingSlotReversal.naturalProduct value U : ℤ)) *
        movingGiantUnitPeriod value outside left * movingGiantUnitPeriod value outside right

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

theorem OAI.Ostmann.movingLocalGiantUnits_modEq line 86
theorem OAI.Ostmann.movingSignedGiantUnits_modEq line 105