AllocationOutputs.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Exact two child-output rules of companion §05. The estimates retain one copy of the parent variation; this coefficient must be independent of k for the tree absorption. Input inequalities below are the explicit rank, cap, and proportion conditions, not an assumed output feasibility statement.

def OAI.UniformKServer.AllocationOutputs.lower line 17
def OAI.UniformKServer.AllocationOutputs.excess line 19
def OAI.UniformKServer.AllocationOutputs.ruleOne line 21
def OAI.UniformKServer.AllocationOutputs.ruleTwo line 23
def OAI.UniformKServer.AllocationOutputs.variation line 26
theorem OAI.UniformKServer.AllocationOutputs.excess_nonneg line 29
theorem OAI.UniformKServer.AllocationOutputs.required_holes line 32
theorem OAI.UniformKServer.AllocationOutputs.rule_one_budget line 49
theorem OAI.UniformKServer.AllocationOutputs.rule_one_upper line 58

theorem OAI.UniformKServer.AllocationOutputs.rule_one_regular line 65

Source documentation

Source Rule I, at regular coordinates. The error comparison e≤εS includes the admissible zero case S=0, so no division by S is used.

theorem rule_one_regular (n B f b β η α : ι → ℝ) (βv q e ε : ℝ)
    (hB : ∀ i, 0 ≤ B i) (hα : ∀ i, 0 ≤ α i)
    (hβ : 0 ≤ βv+ε)
    (hR : excess (fun i => n i+b i) q ≤ βv*(∑ i, B i)+e)
    (he : e ≤ ε*(∑ i, B i))
    (hprop : ∀ i, (∑ j, B j)*α i ≤ (1+η i)*B i)
    (i : ι) (hgap : (βv+ε)*(1+η i) ≤ β i) (hcap : f i ≤ b i) :
    lower n B f β i ≤ ruleOne (fun i => n i+b i) α q i := by
…

Mentions: OAI.UniformKServer.AllocationOutputs.excess, OAI.UniformKServer.AllocationOutputs.lower, OAI.UniformKServer.AllocationOutputs.ruleOne

theorem OAI.UniformKServer.AllocationOutputs.rule_one_dominant line 83

Source documentation

Source Rule I at the marked dominant coordinate: the cap's excess e is retained without multiplying it by a inverse core mass.

theorem rule_one_dominant (n B f b β η α : ι → ℝ) (βv q e : ℝ)
    (hB : ∀ i, 0 ≤ B i) (hα : ∀ i, 0 ≤ α i) (hαsum : (∑ i, α i)=1)
    (hβ : 0 ≤ βv) (he : 0 ≤ e)
    (hR : excess (fun i => n i+b i) q ≤ βv*(∑ i, B i)+e)
    (hprop : ∀ i, (∑ j, B j)*α i ≤ (1+η i)*B i)
    (o : ι) (hgap : βv*(1+η o) ≤ β o) (hcap : f o+e ≤ b o) :
    lower n B f β o ≤ ruleOne (fun i => n i+b i) α q o := by
…

Mentions: OAI.UniformKServer.AllocationOutputs.excess, OAI.UniformKServer.AllocationOutputs.lower, OAI.UniformKServer.AllocationOutputs.ruleOne

theorem OAI.UniformKServer.AllocationOutputs.rule_two_side line 100
theorem OAI.UniformKServer.AllocationOutputs.rule_two_budget line 103
theorem OAI.UniformKServer.AllocationOutputs.rule_two_upper line 115

theorem OAI.UniformKServer.AllocationOutputs.rule_two_lower line 127

Source documentation

Exact lower bounds of Rule II, with the side lower tracker inequality and the aggregate side slack paid from the dominant parameter gap.

theorem rule_two_lower (n B fp fc b β : ι → ℝ) (w θ z : ι → ℝ)
    (q D βv βplus : ℝ) (o : ι)
    (hB : ∀ i, 0 ≤ B i) (hparent : (∑ i, (n i-βv*B i+fp i)) ≤ q)
    (hparam : βv ≤ βplus)
    (hcap : ∀ i, fc i ≤ b i)
    (hsideCap : ∀ i, i ≠ o → b i ≤ fp i)
    (hupper : ∀ i, i ≠ o → D*w i ≤ β i*B i)
    (hlower : ∀ i, i ≠ o → βplus*B i-D*θ i*z i ≤ D*w i)
    (hslack : D*(∑ i ∈ univ.erase o, θ i*z i) ≤
      (n o-βv*B o+fp o)-lower n B fc β o)
    (hβo : 0 ≤ β o) :
    ∀ i, lower n B fc β i ≤ ruleTwo (fun i => n i+b i) w q D o i := by
…

Mentions: OAI.UniformKServer.AllocationOutputs.lower, OAI.UniformKServer.AllocationOutputs.ruleTwo