OAI/Combinatorics/UniformKServer/EpochParameters.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Parameters on the actual positive held-size domain of one vector epoch. These are the geometric hypotheses of the logarithmic proportion minimizer.

  1. def OAI.UniformKServer.EpochParameters.active line 18
  2. theorem OAI.UniformKServer.EpochParameters.mem_active line 22
  3. theorem OAI.UniformKServer.EpochParameters.active_sum line 26
  4. theorem OAI.UniformKServer.EpochParameters.exp_height line 38
  5. theorem OAI.UniformKServer.EpochParameters.exp_height_le line 46
  6. theorem OAI.UniformKServer.EpochParameters.regular_height line 52
  7. theorem OAI.UniformKServer.EpochParameters.active_total_pos line 60
  8. theorem OAI.UniformKServer.EpochParameters.regular_exponential_sum line 69
  9. theorem OAI.UniformKServer.EpochParameters.side_nonneg line 79
  10. theorem OAI.UniformKServer.EpochParameters.side_coordinate line 85
  11. def OAI.UniformKServer.EpochParameters.sideReference line 92
  12. theorem OAI.UniformKServer.EpochParameters.marked_u_upper line 96
  13. theorem OAI.UniformKServer.EpochParameters.marked_height_lower line 107

    Source documentation

    The logarithmic side weight controls the approaching-simplex-vertex height. The estimate keeps the factor independent of the number of inactive children.

    theorem marked_height_lower {A ai U : ℝ} (hA : 0 < A) (hai : 0 < ai)
    (haiU : ai ≤ (1001/1000)*U) (hu : U/A ≤ 1) (hU : 0 < U) :
    (1/2)*(1+Real.log (1/(U/A))) ≤ SideParameters.height A ai := by
…

    Mentions: OAI.UniformKServer.SideParameters.height

  14. theorem OAI.UniformKServer.EpochParameters.side_exp_sum line 124