OAI/Analysis/PathSelection/RelativeErrors.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Relative perturbation errors, modulus estimates and zero-exponent charts.

  1. lemma OAI.DegeneratingTrees.Clock.tendsto_sectorInfinity_of_close_map line 16
  2. lemma OAI.DegeneratingTrees.Clock.baseLoss_le_of_upper line 31
  3. theorem OAI.DegeneratingTrees.Clock.sector_relative_perturbation line 46
  4. theorem OAI.DegeneratingTrees.Clock.zero_exponent_relative_error line 77
  5. lemma OAI.DegeneratingTrees.Clock.nearIdentity_norm_bounds line 104
  6. theorem OAI.DegeneratingTrees.Clock.relative_error_comp_nearIdentity line 116
  7. lemma OAI.DegeneratingTrees.Clock.sector_principal_log_bound line 147
  8. lemma OAI.DegeneratingTrees.Clock.littleO_baseLoss_tendsto_zero line 171
  9. theorem OAI.DegeneratingTrees.Clock.nearIdentity_factor_ratio line 179
  10. lemma OAI.DegeneratingTrees.Clock.relative_modulus_bounds line 208
  11. theorem OAI.DegeneratingTrees.Clock.relative_modulus_comparison line 223
  12. theorem OAI.DegeneratingTrees.Clock.zero_exponent_chart line 250