OAI/Combinatorics/UniformKServer/SideParameters.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact held side parameters and their uniform logarithmic bounds, companion §04. No lower bound on a side proportion and no cardinality factor is used.

  1. def OAI.UniformKServer.SideParameters.height line 13
  2. def OAI.UniformKServer.SideParameters.offset line 14
  3. def OAI.UniformKServer.SideParameters.slack line 15
  4. theorem OAI.UniformKServer.SideParameters.height_ge_one line 17
  5. theorem OAI.UniformKServer.SideParameters.offset_pos line 22
  6. theorem OAI.UniformKServer.SideParameters.offset_inverse line 27
  7. theorem OAI.UniformKServer.SideParameters.log_bound line 35

    Source documentation

    The side logarithm is at most (W+2)h throughout its compact domain.

    theorem log_bound {A a s W : ℝ} (ha : 0 < a) (haA : a ≤ A)
    (hs : 0 ≤ s) (hsW : s ≤ W) :
    Real.log (1+s/offset A a) ≤ (W+2)*height A a := by
…

    Mentions: OAI.UniformKServer.SideParameters.offset, OAI.UniformKServer.SideParameters.height

  8. theorem OAI.UniformKServer.SideParameters.slack_pos line 57
  9. theorem OAI.UniformKServer.SideParameters.inverse_slack line 62
  10. theorem OAI.UniformKServer.SideParameters.logarithm_over_slack line 72