OAI/Geometry/TamingCompatibility/HeatFlow/HodgeHeatSmoothing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.hodgeBoundedSpectralMultiplier line 18
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeBoundedSpectralMultiplier_repr line 30
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeBoundedSpectralMultiplier_eigenvector line 40
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeBoundedSpectralMultiplier_norm_le line 62
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeBoundedSpectralMultiplier_symmetric line 78
6. lemma OAI.TamingCompatibility.GeometricHilbert.heat_boost_bound line 93
7. def OAI.TamingCompatibility.GeometricHilbert.hodgeHeatBoost line 105
8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_factor line 111
9. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeHeatBoost_norm_le line 173