OAI/NumberTheory/JointDickman/Analysis/LogPhaseTerminalBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Scalar bounds for logarithmic terminal sums

These two elementary real inequalities are reused from the frozen internal reciprocal-phase proof, with their names changed to the present application.

  1. theorem OAI.JointDickman.logarithmic_terminal_error_bound line 12
  2. theorem OAI.JointDickman.logarithmic_terminal_sqrt_budget line 46