OAI/NumberTheory/Ostmann/Construction/ConstituentHProductLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A lower endpoint for the actual supported H product

  1. def OAI.Ostmann.ConstituentHProductLower line 10

    Source documentation

    The endpoint is required only where the full inherited coefficient is live.

    def ConstituentHProductLower {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ)
    (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
    (leaf : ScheduleAtomState role → ℤ → ℂ) (Z : ℝ) : Prop :=
…

    Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState

  2. theorem OAI.Ostmann.constituentHProductLower_of_atom_intervals line 23