OAI/Analysis/PathSelection/CoefficientFields.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Local sectors, lower sector data and fields of expansion coefficients.

  1. lemma OAI.DegeneratingTrees.sector_eventually_nhds line 16
  2. lemma OAI.DegeneratingTrees.sector_eventually_analytic_congr line 23
  3. lemma OAI.DegeneratingTrees.sector_eventually_deriv_congr line 29
  4. lemma OAI.DegeneratingTrees.Clock.SectorExpansion.congr line 36
  5. structure OAI.DegeneratingTrees.Clock.LowerSectorData line 55
  6. lemma OAI.DegeneratingTrees.Clock.LowerSectorData.finset_sum_mem line 70
  7. lemma OAI.DegeneratingTrees.Clock.LowerSectorData.word_mem line 79
  8. lemma OAI.DegeneratingTrees.Clock.LowerSectorData.geometric_mem line 87
  9. lemma OAI.DegeneratingTrees.Clock.LowerSectorData.convolution_mem line 94
  10. def OAI.DegeneratingTrees.Clock.ExpansionOver line 104
  11. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.const line 111
  12. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.congr line 115
  13. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.neg line 120
  14. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.add line 124
  15. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.mul line 139
  16. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.inverse_of_leading line 147
  17. theorem OAI.DegeneratingTrees.Clock.ExpansionOver.inv line 195