OAI/Analysis/PathSelection/SectorUniqueness.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of holomorphic asymptotic expansions on sectors.

  1. def OAI.DegeneratingTrees.quadraticRegion line 18
  2. def OAI.DegeneratingTrees.lossSector line 22
  3. def OAI.DegeneratingTrees.AdmissibleAngularLoss line 27
  4. def OAI.DegeneratingTrees.CentralSuperexponential line 35
  5. def OAI.DegeneratingTrees.SectorUniquenessStatement line 42
  6. def OAI.DegeneratingTrees.sectorKernel line 52
  7. lemma OAI.DegeneratingTrees.kernel_den_ne line 54
  8. lemma OAI.DegeneratingTrees.sectorKernel_norm_le line 61
  9. lemma OAI.DegeneratingTrees.sectorKernel_re_nonneg line 69
  10. lemma OAI.DegeneratingTrees.mul_sectorKernel_re line 75
  11. lemma OAI.DegeneratingTrees.mul_sectorKernel_re_nonneg line 83
  12. lemma OAI.DegeneratingTrees.mul_sectorKernel_re_lower line 88
  13. lemma OAI.DegeneratingTrees.arg_lt_of_re_lower line 104
  14. def OAI.DegeneratingTrees.sectorCorrection line 116
  15. def OAI.DegeneratingTrees.sectorMap line 119
  16. lemma OAI.DegeneratingTrees.sectorTerm_norm_le line 127
  17. lemma OAI.DegeneratingTrees.sectorTerms_summable line 132
  18. lemma OAI.DegeneratingTrees.sectorCorrection_norm_le line 136
  19. lemma OAI.DegeneratingTrees.sectorCorrection_re_nonneg line 142
  20. lemma OAI.DegeneratingTrees.sectorMap_norm_lower line 150
  21. lemma OAI.DegeneratingTrees.sectorMap_norm_upper line 158
  22. lemma OAI.DegeneratingTrees.sectorMap_re_lower line 166
  23. lemma OAI.DegeneratingTrees.sectorCorrection_differentiableOn line 189
  24. lemma OAI.DegeneratingTrees.sectorMap_differentiableOn line 200
  25. lemma OAI.DegeneratingTrees.dyadic_shell line 206
  26. lemma OAI.DegeneratingTrees.angularLoss_kernel_data line 219
  27. lemma OAI.DegeneratingTrees.sectorMap_arg_real line 289
  28. lemma OAI.DegeneratingTrees.sectorMap_mem_lossSector line 304
  29. lemma OAI.DegeneratingTrees.lossSector_isPreconnected line 330
  30. lemma OAI.DegeneratingTrees.superpolynomialDecay_of_ray_bounds line 375
  31. theorem OAI.DegeneratingTrees.sector_uniqueness line 396