OAI/Analysis/PathSelection/SectorInduction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Transported lower charts, clock-sector induction and universal Hardy calculus.

  1. lemma OAI.DegeneratingTrees.Clock.SectorInverse.original_ray line 16
  2. lemma OAI.DegeneratingTrees.Clock.ScalarSectorChart.congr_composition line 27
  3. lemma OAI.DegeneratingTrees.Clock.transported_lowerSectorCharts line 40
  4. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.of_lower line 148
  5. structure OAI.DegeneratingTrees.Clock.ClockSectorData line 154
  6. lemma OAI.DegeneratingTrees.Clock.ClockSectorData.expansion_iff line 164
  7. lemma OAI.DegeneratingTrees.Clock.puiseux_clockSectorData line 173
  8. lemma OAI.DegeneratingTrees.Clock.ClockSectorData.step line 196
  9. theorem OAI.DegeneratingTrees.Clock.ValidClocks.sectorData line 262
  10. lemma OAI.DegeneratingTrees.Clock.ClockGerm.of_lower line 282
  11. theorem OAI.DegeneratingTrees.Clock.ClockGerm.inv line 291
  12. theorem OAI.DegeneratingTrees.Clock.ClockGerm.deriv line 302
  13. lemma OAI.DegeneratingTrees.Clock.ClockGerm.real_deriv line 326
  14. theorem OAI.DegeneratingTrees.Clock.ClockGerm.real_derivative_sign line 334
  15. lemma OAI.DegeneratingTrees.Clock.LogMonomial.rat_mul line 353
  16. lemma OAI.DegeneratingTrees.Clock.puiseux_exp_rat_log line 367
  17. lemma OAI.DegeneratingTrees.Clock.ClockGerm.exp_clock line 377
  18. lemma OAI.DegeneratingTrees.Clock.LogMonomial.exp_mem line 389
  19. theorem OAI.DegeneratingTrees.Clock.ClockGerm.divisible_size line 401
  20. theorem OAI.DegeneratingTrees.Clock.ClockGerm.eventually_monotone line 435