OAI/Analysis/PathSelection/RecursiveCharts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

General common charts, second-clock charts and slowly varying coefficients.

  1. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.zero_chart line 16
  2. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.scalar_chart line 139
  3. lemma OAI.DegeneratingTrees.Clock.ScalarSectorChart.congr_inverse line 164
  4. lemma OAI.DegeneratingTrees.Clock.lowerSectorData_hasSectorCharts line 178
  5. lemma OAI.DegeneratingTrees.Clock.ExpBound.comp_slow line 206
  6. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.expBound_some line 233
  7. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.zero_or_ne line 239
  8. def OAI.DegeneratingTrees.Clock.TransportedFirstField line 257
  9. lemma OAI.DegeneratingTrees.Clock.transported_first_lowerSectorData line 260
  10. lemma OAI.DegeneratingTrees.Clock.puiseux_variable line 302
  11. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.puiseux_mem line 307
  12. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.lower_field_chart line 313
  13. lemma OAI.DegeneratingTrees.Clock.transported_first_iff line 339
  14. lemma OAI.DegeneratingTrees.Clock.finite_strict_gap line 376
  15. theorem OAI.DegeneratingTrees.Clock.SectorExpansion.coefficient_slow line 395