OAI/NumberTheory/EgyptianFractions/TerminalDepth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.TerminalDepth.depth line 9

   Source documentation

   Number of contractions reducing a logarithmic height S to one.

   def depth (α S : ℝ) : ℕ := ⌈Real.log S / (-Real.log α)⌉₊

2. theorem OAI.Problem337.TerminalDepth.depth_contracts line 11
3. theorem OAI.Problem337.TerminalDepth.depth_budget line 22
4. def OAI.Problem337.TerminalDepth.binaryExponent line 35

   Source documentation

   The base-two exponent needed by the terminal binary range.

   def binaryExponent (D S : ℝ) : ℕ := ⌈D * Real.log S / Real.log 2⌉₊

   Mentions: OAI.Problem337.D

5. theorem OAI.Problem337.TerminalDepth.binary_log_lower line 37
6. theorem OAI.Problem337.TerminalDepth.terminal_length_budget line 45
7. theorem OAI.Problem337.TerminalDepth.potential_bound line 68
8. theorem OAI.Problem337.TerminalDepth.rpow_le_binary line 79