OAI/NumberTheory/Ostmann/Arithmetic/ForwardHistorySupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The constructed adaptive support for actual forward giant coefficients

  1. def OAI.Ostmann.forwardNodeGiants line 13
  2. def OAI.Ostmann.forwardIntegerHistory line 22

    Source documentation

    The actual node equations use the fixed nonbulk factor and the current giant on each child. The support includes both coefficient unit conditions.

    def forwardIntegerHistory (S : Finset ℤ) (n Q : ℕ) (t : FrequencyTree S n)
    (XL XR : ℤ) (CL CR : List Bool → ℤ) (a : SampledPivotHistory n Q) : Prop :=
…

    Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.SampledPivotHistory

  3. theorem OAI.Ostmann.forwardIntegerHistory_valid line 32
  4. theorem OAI.Ostmann.forwardTreeAncestorScheme_depth line 44
  5. theorem OAI.Ostmann.forwardTreeAncestorScheme_root_ne_zero line 49
  6. theorem OAI.Ostmann.forwardTreeAncestorScheme_frequency_dvd line 55