OAI/Analysis/PathSelection/InverseEstimates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Inverse derivative absorption, exponential decay and comparable inverse charts.

  1. lemma OAI.DegeneratingTrees.Clock.summable_abs_variation line 16
  2. theorem OAI.DegeneratingTrees.Clock.derivative_summable_unit_shells line 33
  3. theorem OAI.DegeneratingTrees.Clock.inverse_derivative_loss_absorption line 157
  4. theorem OAI.DegeneratingTrees.Clock.inverse_exponential_decay line 192
  5. theorem OAI.DegeneratingTrees.Clock.inverse_exponential_loss_absorption line 221
  6. lemma OAI.DegeneratingTrees.Clock.realpart_of_ratio_error line 252
  7. theorem OAI.DegeneratingTrees.Clock.strict_loss_realpart_separation line 266
  8. theorem OAI.DegeneratingTrees.Clock.equal_exponent_realpart_separation line 310
  9. theorem OAI.DegeneratingTrees.Clock.inverse_chart_data line 376
  10. theorem OAI.DegeneratingTrees.Clock.inverse_strip_exponential_error line 436