OAI/Analysis/PathSelection/AdmissibleFunctions.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Real-holomorphic representatives, recursively extracted coefficients and admissibility.

  1. abbrev OAI.PathSelection.Statement.RealPoint line 13
  2. abbrev OAI.PathSelection.Statement.ComplexPoint line 14
  3. def OAI.PathSelection.Statement.complexify line 17
  4. def OAI.PathSelection.Statement.conjugate line 20
  5. def OAI.PathSelection.Statement.realValue line 25
  6. def OAI.PathSelection.Statement.quadraticRegion line 29
  7. def OAI.PathSelection.Statement.tailBand line 32
  8. def OAI.PathSelection.Statement.ordinaryPolydisc line 35
  9. def OAI.PathSelection.Statement.ordinaryClosedPolydisc line 38
  10. def OAI.PathSelection.Statement.quadraticDomain line 43
  11. def OAI.PathSelection.Statement.quadraticEstimateDomain line 48
  12. def OAI.PathSelection.Statement.commonBandDomain line 53
  13. def OAI.PathSelection.Statement.RealHolomorphicOn line 57
  14. structure OAI.PathSelection.Statement.Extraction line 63
  15. def OAI.PathSelection.Statement.expanded line 68
  16. structure OAI.PathSelection.Statement.CoefficientSystem line 72
  17. def OAI.PathSelection.Statement.CoefficientSystem.Valid line 79
  18. def OAI.PathSelection.Statement.CoefficientSystem.IndependentOfExpanded line 87
  19. def OAI.PathSelection.Statement.CoefficientSystem.QuadraticallyBounded line 93
  20. def OAI.PathSelection.Statement.CoefficientSystem.finiteSum line 102
  21. def OAI.PathSelection.Statement.CoefficientSystem.singlePartialSum line 107
  22. def OAI.PathSelection.Statement.CoefficientSystem.SingleExpansion line 116
  23. def OAI.PathSelection.Statement.CoefficientSystem.iteratedHistories line 129
  24. def OAI.PathSelection.Statement.CoefficientSystem.weight line 133
  25. def OAI.PathSelection.Statement.CoefficientSystem.iteratedTerm line 136
  26. def OAI.PathSelection.Statement.CoefficientSystem.groupedPartialSum line 141
  27. def OAI.PathSelection.Statement.CoefficientSystem.GroupedExpansion line 149
  28. def OAI.PathSelection.Statement.CoefficientSystem.CommonCoefficientDomains line 168
  29. def OAI.PathSelection.Statement.Admissible line 178
  30. inductive OAI.PathSelection.Statement.SignFormula line 188
  31. def OAI.PathSelection.Statement.SignFormula.Holds line 198
  32. def OAI.PathSelection.Statement.EventuallyMonotoneOrConstant line 210
  33. def OAI.PathSelection.Statement.PathConclusion line 216
  34. lemma OAI.PathSelection.Statement.realValue_eq_of_realHolomorphicOn line 232
  35. lemma OAI.PathSelection.Statement.eventually_mem_quadraticDomain line 244
  36. lemma OAI.PathSelection.Statement.Admissible.eventually_realValue_eq line 267