OAI/Combinatorics/UniformKServer/OffsetLP.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite additive-offset variant of the same exact rational flow system. The source permits an arbitrarily large instance-dependent initialization delay. This auxiliary system allows its horizon-independent finite-law endpoint to be absorbed in a sufficiently long restart epoch; no main conclusion is assumed. All original source definitions and their coefficient optimizer are unchanged.

  1. def OAI.UniformKServer.OffsetLP.constraints line 16
  2. def OAI.UniformKServer.OffsetLP.Valid line 39

    Source comment

    Exact interpretation of the source constraints, over either rationals or reals.
    def Valid {n k H : ℕ} {K : Type*} [Field K] [LinearOrder K]
    (d : RationalMetric n) (u : Config n k) (A : ℚ) (F : BoundedFlow n k H K) (a : K)
    [NeZero k] : Prop :=
…

    Mentions: OAI.UniformKServer.RationalMetric

  3. theorem OAI.UniformKServer.OffsetLP.constraints_iff line 53
  4. theorem OAI.UniformKServer.OffsetLP.rational_attainment line 93