OAI/NumberTheory/Ostmann/Construction/InitialMovingData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The original cutoff weight as a function of the actual leaf data

  1. def OAI.Ostmann.initialRegularFromList line 11
  2. theorem OAI.Ostmann.initialRegularFromList_mapped line 15
  3. def OAI.Ostmann.initialMovingDataCutoff line 29

    Source documentation

    Internal states use the same total function, while only terminal data are evaluated as leaves. The fallback is never used on a genuine template.

    noncomputable def initialMovingDataCutoff {P : Type*} (value : P → ℕ) (b d r : ℕ)
    (cb cd : ℝ) (sl sr : Fin d → P) (fallback : P) :
    {n : ℕ} → MovingSlotData P n → ℤ → ℂ :=
…

    Mentions: OAI.Ostmann.MovingSlotData

  4. theorem OAI.Ostmann.initialMovingDataCutoff_zero line 36
  5. theorem OAI.Ostmann.initialMovingDataCutoff_leaf line 41
  6. theorem OAI.Ostmann.initialMovingState_modulus line 51
  7. theorem OAI.Ostmann.initialMovingLeaf_value line 63