CrossRule.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The two actual hysteresis crossings in the star outputs. In contrast to comparing with an unused old rule, these bounds use only the states that actually existed. The coefficient of parent variation stays exactly one.

theorem OAI.UniformKServer.AllocationOutputs.holes_two_nonneg line 17
theorem OAI.UniformKServer.AllocationOutputs.holes_two_total line 24
theorem OAI.UniformKServer.AllocationOutputs.nonnegative_movement line 39
theorem OAI.UniformKServer.AllocationOutputs.side_scalar_bound line 46
theorem OAI.UniformKServer.AllocationOutputs.rule_two_eq_holes line 56

theorem OAI.UniformKServer.AllocationOutputs.downcross line 63

Source documentation

I-to-II: the new D suffices, even though no old side vector was output.

theorem downcross (d₀ d₁ α₀ w₁ : ι → ℝ) (q₀ q₁ D₁ L W : ℝ) (o : ι)
    (hα : ∀ i, 0 ≤ α₀ i) (hsum : ∑ i, α₀ i=1)
    (hD : 0 ≤ D₁) (hw : ∀ i, 0 ≤ w₁ i) (hW : ∑ i, w₁ i ≤ W)
    (hR : excess d₁ q₁ ≤ L*D₁) :
    variation (ruleOne d₀ α₀ q₀) (ruleTwo d₁ w₁ q₁ D₁ o) ≤
      |q₁-q₀|+2*variation d₀ d₁+(2*L+W)*D₁ := by
…

Mentions: OAI.UniformKServer.AllocationOutputs.excess, OAI.UniformKServer.AllocationOutputs.variation, OAI.UniformKServer.AllocationOutputs.ruleOne, OAI.UniformKServer.AllocationOutputs.ruleTwo

theorem OAI.UniformKServer.AllocationOutputs.upcross line 91

Source documentation

II-to-I: the new S plus held-D variation suffices, without evaluating the old simplex state as though Rule I had been in force there.

theorem upcross (d₀ d₁ w₀ α₁ : ι → ℝ) (q₀ q₁ D₀ D₁ S₁ L W : ℝ) (o : ι)
    (hα : ∀ i, 0 ≤ α₁ i) (hsum : ∑ i, α₁ i=1)
    (hD₀ : 0 ≤ D₀) (hw : ∀ i, 0 ≤ w₀ i) (hW : ∑ i, w₀ i ≤ W)
    (hR : excess d₁ q₁ ≤ L*S₁) (hSD : D₁ ≤ S₁/2) :
    variation (ruleTwo d₀ w₀ q₀ D₀ o) (ruleOne d₁ α₁ q₁) ≤
      |q₁-q₀|+2*variation d₀ d₁+(2*L+W/2)*S₁+W*|D₁-D₀| := by
…

Mentions: OAI.UniformKServer.AllocationOutputs.excess, OAI.UniformKServer.AllocationOutputs.variation, OAI.UniformKServer.AllocationOutputs.ruleTwo, OAI.UniformKServer.AllocationOutputs.ruleOne