OAI/Analysis/PathSelection/SectorBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Cauchy estimates, sector narrowing, tails and subexponential losses.

  1. lemma OAI.DegeneratingTrees.AdmissibleAngularLoss.real_discs line 17
  2. lemma OAI.DegeneratingTrees.sector_deriv_ray_bound line 45
  3. def OAI.DegeneratingTrees.windowSum line 78
  4. lemma OAI.DegeneratingTrees.window_bound line 80
  5. def OAI.DegeneratingTrees.neighboringLoss line 120
  6. lemma OAI.DegeneratingTrees.neighboringLoss_tail_bdd line 122
  7. lemma OAI.DegeneratingTrees.AdmissibleAngularLoss.neighboring line 141
  8. lemma OAI.DegeneratingTrees.AdmissibleAngularLoss.const_mul line 162
  9. lemma OAI.DegeneratingTrees.log_margin_grows line 173
  10. lemma OAI.DegeneratingTrees.half_loss_norm_le_re line 186
  11. theorem OAI.DegeneratingTrees.AdmissibleAngularLoss.narrow_discs line 204
  12. theorem OAI.DegeneratingTrees.sector_deriv_bound line 253
  13. lemma OAI.DegeneratingTrees.AdmissibleAngularLoss.max line 290
  14. def OAI.DegeneratingTrees.SectorEventually line 308
  15. lemma OAI.DegeneratingTrees.SectorEventually.mono line 311
  16. lemma OAI.DegeneratingTrees.SectorEventually.and line 316
  17. lemma OAI.DegeneratingTrees.SectorEventually.finset_forall line 327
  18. theorem OAI.DegeneratingTrees.sector_zero_of_ray_zero line 341
  19. lemma OAI.DegeneratingTrees.AdmissibleAngularLoss.tendsto_zero line 384
  20. lemma OAI.DegeneratingTrees.AdmissibleAngularLoss.power_absorption line 405
  21. def OAI.DegeneratingTrees.baseLoss line 441
  22. lemma OAI.DegeneratingTrees.admissible_baseLoss line 443
  23. lemma OAI.DegeneratingTrees.SectorEventually.of_radial line 468
  24. lemma OAI.DegeneratingTrees.SectorEventually.truth line 473
  25. lemma OAI.DegeneratingTrees.SectorEventually.realpart_pos line 476