OAI/Analysis/PathSelection/PhaseSectors.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Positive Puiseux sectors, loss scales and strict phase estimates.

  1. lemma OAI.DegeneratingTrees.Clock.analytic_root_error line 17
  2. theorem OAI.DegeneratingTrees.Clock.Puiseux.positive_sector line 28
  3. def OAI.DegeneratingTrees.scaleEnvelope line 86
  4. lemma OAI.DegeneratingTrees.scale_window_bound line 89
  5. lemma OAI.DegeneratingTrees.scale_envelope_bdd line 126
  6. lemma OAI.DegeneratingTrees.AdmissibleAngularLoss.scale_envelope line 147
  7. lemma OAI.DegeneratingTrees.Clock.cpow_real_re line 190
  8. lemma OAI.DegeneratingTrees.Clock.cpow_real_re_lower line 199
  9. lemma OAI.DegeneratingTrees.Clock.power_error_relative line 211
  10. lemma OAI.DegeneratingTrees.Clock.power_model_norm line 220
  11. theorem OAI.DegeneratingTrees.Clock.power_model_sublinear_sector line 240
  12. lemma OAI.DegeneratingTrees.Clock.phase_ratio_error line 287
  13. theorem OAI.DegeneratingTrees.Clock.strict_phase_sector_mapping line 310
  14. theorem OAI.DegeneratingTrees.Clock.sublinear_sector_realpart line 388
  15. theorem OAI.DegeneratingTrees.Clock.sector_sublinear_realpart line 446