OAI/Combinatorics/UniformKServer/ParentBeta.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A concrete admissible absolute logarithmic coefficient and the parent's held upper parameter. The source permits any sufficiently small positive absolute coefficient; this choice preserves its parameter formula.

  1. def OAI.UniformKServer.ParentBeta.cBeta line 18
  2. def OAI.UniformKServer.ParentBeta.param line 20
  3. def OAI.UniformKServer.ParentBeta.trueParam line 22
  4. def OAI.UniformKServer.ParentBeta.heldParam line 24
  5. theorem OAI.UniformKServer.ParentBeta.param_allowed line 26
  6. theorem OAI.UniformKServer.ParentBeta.true_allowed line 56
  7. theorem OAI.UniformKServer.ParentBeta.held_allowed line 65
  8. theorem OAI.UniformKServer.ParentBeta.parameter_accuracy line 76