OAI/Analysis/C0Absorption/Space.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.baseRepresentation line 14
  2. theorem OAI.C0Absorption.baseRepresentation_value line 19
  3. theorem OAI.C0Absorption.correction_mem_TClass line 24
  4. def OAI.C0Absorption.correctionDualBound line 27
  5. theorem OAI.C0Absorption.correction_pairing_bound line 29
  6. def OAI.C0Absorption.moleculeCorrection line 33
  7. theorem OAI.C0Absorption.moleculeCorrection_apply line 36
  8. def OAI.C0Absorption.initialCorrection line 47
  9. def OAI.C0Absorption.correctionQ line 56
  10. theorem OAI.C0Absorption.correctionQ_coe line 59
  11. theorem OAI.C0Absorption.correctionC0_zero line 64
  12. theorem OAI.C0Absorption.correctionQ_zeta line 68
  13. def OAI.C0Absorption.concreteLift line 75
  14. theorem OAI.C0Absorption.concreteLift_lipschitz line 77
  15. theorem OAI.C0Absorption.concreteLift_zero line 80
  16. theorem OAI.C0Absorption.concreteLift_homogeneous line 82
  17. theorem OAI.C0Absorption.correctionQ_concreteLift line 85