OAI/NumberTheory/Ostmann/Characters/CharacterSelectionBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A single depth choice pays for all actual cell-selection codes

  1. def OAI.Ostmann.characterTargetLabelBound line 10
  2. theorem OAI.Ostmann.character_target_label_bound line 13
  3. theorem OAI.Ostmann.character_selection_code_bound line 30
  4. theorem OAI.Ostmann.character_selection_depth line 47

    Source documentation

    This threshold precedes the density increment and is uniform over the resulting depth, endpoint tests, target values and selected word lengths.

    theorem character_selection_depth (c δ C b : ℝ) (hc : 0 < c) (hδ : 0 < δ)
    (hb : 0 < b) (Kmin : ℕ) :
    ∃ K : ℕ, Kmin ≤ K ∧ ∀ k : ℕ, K ≤ k →
      1 ≤ k ∧ 1 ≤ cellRoleScale k ∧
      C + 20 * Real.log (cellRoleScale k) ≤ (k : ℝ) * Real.log 2 - 1 ∧
      ((characterTargetLabelBound c δ k + (k + 1) + (k + 1) : ℕ) : ℝ) ≤ b * cellRoleScale k := by
…

    Mentions: OAI.Ostmann.cellRoleScale, OAI.Ostmann.characterTargetLabelBound