OAI/Combinatorics/UniformKServer/ActualRoster.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.ActualRoster.survival line 16
  2. def OAI.UniformKServer.ActualRoster.valid line 18
  3. def OAI.UniformKServer.ActualRoster.active line 23
  4. def OAI.UniformKServer.ActualRoster.compulsory line 26
  5. def OAI.UniformKServer.ActualRoster.next line 29
  6. def OAI.UniformKServer.ActualRoster.retires line 39

    Source documentation

    Only an old selected covering record can trigger this event. The selector may depend on the entire old roster and its persistent radii, but not on the fresh lifetime trials.

    def retires (D : State I) (S : Finset I) (c : I → X) (r : ℝ) (K : ℕ)
    (n : I) (select : D.Sample → Option I) (ω : D.Sample) (τ : I → Bool) : Prop :=
…
  7. theorem OAI.UniformKServer.ActualRoster.survival_zero line 44
  8. theorem OAI.UniformKServer.ActualRoster.survival_step line 49
  9. theorem OAI.UniformKServer.ActualRoster.empty_valid line 65
  10. theorem OAI.UniformKServer.ActualRoster.next_marginal line 73
  11. theorem OAI.UniformKServer.ActualRoster.next_valid line 89
  12. theorem OAI.UniformKServer.ActualRoster.conditional_retirement line 138
  13. theorem OAI.UniformKServer.ActualRoster.first_retirement line 199

    Source documentation

    Source actual-retirement-bound, including arbitrary data-dependent first coverer and the exact locality cutoff. Survival is averaged over the old law, not falsely conditioned on a realized surviving old roster.

    theorem first_retirement (D : State I) (S : Finset I) (c : I → X) (r : ℝ)
    (hr : 0 < r) (K : ℕ) (hK : 2 ≤ K) (hq : 1/(K:ℝ) ∈ Set.Icc (0:ℝ) 1)
    (n : I) (hD : valid D S c r K) (p : X) (select : D.Sample → Option I)
    (hcover : ∀ ω i, select ω = some i → dist p (c i) ≤ 2*r) :
    (D.law.prod (fresh (I := I) (1/(K:ℝ)) hq)).expect (fun ω =>
…

    Mentions: OAI.UniformKServer.ActualRoster.valid