OAI/Combinatorics/UniformKServer/AlphaRecurrence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A single deterministic selection of the two proven minimizations. This supplies causal states, rather than postulating a trajectory satisfying the desired movement bound. The fallback branch is never used on valid input.

  1. def OAI.UniformKServer.AlphaRecurrence.StepSpec line 18
  2. def OAI.UniformKServer.AlphaRecurrence.initial line 27
  3. def OAI.UniformKServer.AlphaRecurrence.chooseStep line 30
  4. theorem OAI.UniformKServer.AlphaRecurrence.initial_spec line 34
  5. theorem OAI.UniformKServer.AlphaRecurrence.chooseStep_spec line 39
  6. def OAI.UniformKServer.AlphaRecurrence.trajectory line 54
  7. def OAI.UniformKServer.AlphaRecurrence.prepared line 58
  8. def OAI.UniformKServer.AlphaRecurrence.InputValid line 61
  9. theorem OAI.UniformKServer.AlphaRecurrence.trajectory_state line 68
  10. theorem OAI.UniformKServer.AlphaRecurrence.trajectory_step line 77
  11. theorem OAI.UniformKServer.AlphaRecurrence.causal_through line 88

    Source documentation

    Prefix equality suffices for output equality; choices cannot inspect any later input. This directly gives measurability in every finite reveal law.

    theorem causal_through (p q : ℕ → Config ι) (S T B D : ℕ → ι → ℝ) (n : ℕ)
    (hp : ∀ t, t ≤ n → p t=q t) (hS : ∀ t, t < n → S t=T t)
    (hB : ∀ t, t ≤ n → B t=D t) :
    trajectory p S B n=trajectory q T D n := by
…

    Mentions: OAI.UniformKServer.AlphaRecurrence.trajectory