OAI/Analysis/PathSelection/EqualExponentCharts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Phase perturbation and vanishing, positive and constant equal-exponent charts.

  1. lemma OAI.DegeneratingTrees.Clock.arg_mul_near_one line 15
  2. theorem OAI.DegeneratingTrees.Clock.inward_phase_small_perturbation line 39
  3. theorem OAI.DegeneratingTrees.Clock.comparable_sector_mapping line 69
  4. theorem OAI.DegeneratingTrees.Clock.vanishing_equal_exponent_chart line 127
  5. theorem OAI.DegeneratingTrees.Clock.inverse_error_absorption line 258
  6. lemma OAI.DegeneratingTrees.Clock.strict_loss_tendsto_zero line 299
  7. theorem OAI.DegeneratingTrees.Clock.positive_limit_phase line 306
  8. theorem OAI.DegeneratingTrees.Clock.positive_equal_exponent_chart line 361
  9. theorem OAI.DegeneratingTrees.Clock.constant_equal_exponent_chart line 454