OAI/Geometry/TamingCompatibility/Hodge/HodgeL2Coefficients.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.GeometricHilbert.lpEncode line 16
  2. lemma OAI.TamingCompatibility.GeometricHilbert.lpEncode_inner line 33
  3. def OAI.TamingCompatibility.GeometricHilbert.lpEncodeIsometry line 42
  4. def OAI.TamingCompatibility.GeometricHilbert.isometryFromCompletion line 51
  5. lemma OAI.TamingCompatibility.GeometricHilbert.isometryFromCompletion_coe line 61
  6. abbrev OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.HilbertFrame line 78
  7. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalizedFrameEncode line 80
  8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalizedFrameEncode_apply line 86
  9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalizedFrameEncode_inner line 92
  10. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalizedFrameEncode_continuous line 113
  11. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.smoothFrameEncode line 121
  12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.smoothFrameEncode_memLp line 131
  13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.smoothFrameEncode_inner_integral line 139
  14. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.l2Coefficients line 147
  15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.l2Coefficients_smooth line 153
  16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.l2Coefficients_pairing line 165