OAI/Geometry/TamingCompatibility/Hodge/HodgeGlobalEvaluation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationTerm line 29
  2. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluationTerm_continuous line 35
  3. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluation line 59
  4. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.evaluation_continuous line 62
  5. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.continuousEvaluation line 69
  6. def OAI.TamingCompatibility.GeometricHilbert.l2StarIsometry line 87
  7. def OAI.TamingCompatibility.GeometricHilbert.hodgeAmbientStar line 90
  8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeAmbientStar_graph line 95
  9. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeAmbientStar_square line 108
  10. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeAmbientStar_mem line 115
  11. def OAI.TamingCompatibility.GeometricHilbert.hodgeDomainStar line 127
  12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeDomainStar_square line 133
  13. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeInclusion_star line 137
  14. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeDerivative_star_inner line 141
  15. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeDerivative_star_adjoint line 149