OAI/Analysis/Cotype/BivariateSplit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.chebBasis line 11
  2. theorem OAI.Cotype.chebBasis_apply line 15
  3. def OAI.Cotype.chebLow line 18
  4. theorem OAI.Cotype.chebLow_basis line 23
  5. theorem OAI.Cotype.chebLow_degree line 29
  6. theorem OAI.Cotype.chebLow_eq_self line 40
  7. theorem OAI.Cotype.chebLow_expansion line 47
  8. theorem OAI.Cotype.chebLow_bound line 55
  9. def OAI.Cotype.retainedCoefficient line 64
  10. def OAI.Cotype.retainedSectionS line 67
  11. def OAI.Cotype.splitLowS line 71
  12. def OAI.Cotype.splitHighU line 74
  13. def OAI.Cotype.retainedChebCoefficient line 78
  14. theorem OAI.Cotype.retainedSectionS_eval line 82
  15. theorem OAI.Cotype.retainedChebCoefficient_eval line 93
  16. theorem OAI.Cotype.splitLowS_cheb line 105
  17. theorem OAI.Cotype.bivariate_split_eval line 110
  18. theorem OAI.Cotype.splitLowS_degree line 122
  19. theorem OAI.Cotype.splitHighU_degree line 125
  20. theorem OAI.Cotype.splitLowS_bound line 141
  21. theorem OAI.Cotype.splitHighU_bound line 156