OAI/Geometry/TamingCompatibility/Hodge/HodgeSmoothCommutator.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.GeometricHilbert.preAntiProjection line 19
  2. lemma OAI.TamingCompatibility.GeometricHilbert.preAntiProjection_apply line 22
  3. lemma OAI.TamingCompatibility.GeometricHilbert.preAntiProjection_smooth line 26
  4. lemma OAI.TamingCompatibility.GeometricHilbert.preAntiProjection_self_adjoint line 31
  5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeLaplacian_power_symmetric line 38
  6. def OAI.TamingCompatibility.GeometricHilbert.hodgePowerCommutator line 55
  7. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePowerCommutator_apply line 59
  8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgePowerCommutator_skew line 64
  9. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularizedGraph_smoothShift_cube line 72
  10. lemma OAI.TamingCompatibility.linmap_shift_cube line 89
  11. lemma OAI.TamingCompatibility.linmap_shift_cube_commutator line 96
  12. def OAI.TamingCompatibility.GeometricHilbert.hodgeCubeCommutator line 115
  13. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCubeCommutator_expand line 119
  14. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCubeCommutator_skew line 127
  15. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeGraphResolvent_raw_H3 line 152
  16. lemma OAI.TamingCompatibility.GeometricHilbert.exists_hodgeGraphResolvent_H3_lift line 170