OAI/Combinatorics/KServer/Main.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Relabel a finite metric across universes without changing the experiment, initial labels, service constraints, optimal cost or behavior-policy horizon.

  1. lemma OAI.KServer.FiniteMetricTransport.configuration_map line 16
  2. lemma OAI.KServer.FiniteMetricTransport.stronglyLazy line 27
  3. lemma OAI.KServer.FiniteMetricTransport.cost line 39
  4. def OAI.KServer.FiniteMetricTransport.lawOn line 46
  5. lemma OAI.KServer.FiniteMetricTransport.sum_lawOn line 55
  6. lemma OAI.KServer.FiniteMetricTransport.mean_cost line 64
  7. lemma OAI.KServer.FiniteMetricTransport.mean_opt line 73
  8. theorem OAI.KServer.finite_law line 98
  9. def OAI.KServer.MainStatement line 123

    Source documentation

    The positive universal constant strengthens ReductionStatement.

    Distinct definitions of this name: ComparatorChallenges/KServer.lean:51 (same statement text; different proof or body). Qualify references as OAI.KServer.MainStatement@path.

    def MainStatement : Prop :=
…
  10. theorem OAI.KServer.fully_quantified_main line 133
  11. theorem OAI.KServer.main_theorem line 155

    Source documentation

    A positive absolute squared-logarithmic competitive bound on arbitrary metrics, with one causal policy for all horizons and every labeled starting configuration.

    Distinct definitions of this name: ComparatorChallenges/KServer.lean:62 (same statement text; different proof or body). Qualify references as OAI.KServer.main_theorem@path.

    theorem main_theorem : MainStatement.{u} := fully_quantified_main
…

    Mentions: OAI.KServer.fully_quantified_main