OAI/Combinatorics/UniformKServer/EpochAlpha.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Source logarithmic configurations are built on the actual active-size domain, including the automatic one-point domain.

  1. def OAI.UniformKServer.EpochAlpha.ell line 18
  2. theorem OAI.UniformKServer.EpochAlpha.ell_one line 20
  3. theorem OAI.UniformKServer.EpochAlpha.height_upper line 25
  4. def OAI.UniformKServer.EpochAlpha.regular line 44

    Source documentation

    Exact h on all regular coordinates; no clamped-log discrepancy occurs because the epoch geometry proves ai < A.

    def regular (a : ι → ℝ) (A ell ct C : ℝ) : AdaptiveAlpha.Config ι where
…

    Mentions: OAI.UniformKServer.EpochAlpha.ell, OAI.UniformKServer.AdaptiveAlpha.Config

  5. def OAI.UniformKServer.EpochAlpha.marked line 48
  6. def OAI.UniformKServer.EpochAlpha.singleton line 53
  7. theorem OAI.UniformKServer.EpochAlpha.eta_bound line 58
  8. theorem OAI.UniformKServer.EpochAlpha.regular_valid line 65
  9. theorem OAI.UniformKServer.EpochAlpha.marked_valid line 83
  10. theorem OAI.UniformKServer.EpochAlpha.singleton_valid line 145
  11. theorem OAI.UniformKServer.EpochAlpha.side_zero_singleton line 154