OAI/Geometry/TamingCompatibility/HeatFlow/HodgeSpectralHeat.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralSum line 23
  2. def OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralRate line 31
  3. def OAI.TamingCompatibility.GeometricHilbert.hodgeHeatMultiplier line 33
  4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeHeatMultiplier_pos line 35
  5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeHeatMultiplier_le_one line 36
  6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeHeatMultiplier_add line 40
  7. def OAI.TamingCompatibility.GeometricHilbert.hodgeHeatDiagonal line 46
  8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeHeatDiagonal_apply line 57
  9. def OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat line 61
  10. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_repr line 66
  11. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_zero line 76
  12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_add line 84
  13. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_norm_le line 93
  14. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_eigenvector line 103
  15. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeHeatMultiplier_continuous line 141
  16. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_continuous line 144