AlphaEmpty.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Empty active domains are genuine zero states, not a hidden nonempty hypothesis. They occur only at wholesale changes in the derived schedule; the algebra here incurs no restart allowance.

abbrev OAI.UniformKServer.AlphaEmpty.Config line 18
def OAI.UniformKServer.AlphaEmpty.active line 20
def OAI.UniformKServer.AlphaEmpty.valid line 24
def OAI.UniformKServer.AlphaEmpty.state line 28
def OAI.UniformKServer.AlphaEmpty.potential line 32
def OAI.UniformKServer.AlphaEmpty.scale line 36
def OAI.UniformKServer.AlphaEmpty.eta line 40
theorem OAI.UniformKServer.AlphaEmpty.zero_supported line 45
theorem OAI.UniformKServer.AlphaEmpty.exists_state line 50
theorem OAI.UniformKServer.AlphaEmpty.scale_nonneg line 56
theorem OAI.UniformKServer.AlphaEmpty.potential_zero line 62
theorem OAI.UniformKServer.AlphaEmpty.state_interval line 67
theorem OAI.UniformKServer.AlphaEmpty.input_bound line 77
theorem OAI.UniformKServer.AlphaEmpty.update line 84

theorem OAI.UniformKServer.AlphaEmpty.step line 99

Source documentation

Two actual minimizing updates whenever both domains are nonempty. At an empty endpoint, actual zero input supplies the same ledger.

theorem step {p q : Config ι} (hp : valid p) (hq : valid q)
    (Bstar Bnew a₀ : ι → ℝ) (hB : ∀ i, 0 ≤ Bstar i) (hBn : ∀ i, 0 ≤ Bnew i)
    (hST : (∑ i, Bstar i) ≤ ∑ i, Bnew i)
    (hpB : DomainTransport.Supported (active p) Bstar)
    (hqB : DomainTransport.Supported (active q) Bstar)
    (hqN : DomainTransport.Supported (active q) Bnew)
    (ha₀ : state p a₀) :
    ∃ a b, state q a ∧ state q b ∧
      (∀ i, (∑ j, Bnew j)*a i ≤ (1+eta q i)*Bnew i) ∧
      (∀ i, (∑ j, Bstar j)*b i ≤ (1+eta p i)*Bstar i) ∧
      (∑ j, Bnew j)*SimplexTracker.movement a a₀ ≤
        potential p Bstar a₀-potential q Bnew a+
…

Mentions: OAI.UniformKServer.AlphaEmpty.Config, OAI.UniformKServer.AlphaEmpty.valid, OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.AlphaEmpty.active, OAI.UniformKServer.AlphaEmpty.state, OAI.UniformKServer.AlphaEmpty.eta, OAI.UniformKServer.SimplexTracker.movement, OAI.UniformKServer.AlphaEmpty.potential