OAI/Geometry/TamingCompatibility/HeatFlow/HodgeHeatIdentification.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectral_ext line 24
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeBoundedSpectralMultiplier_commutes line 46
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_star line 59
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeBoundedSpectralMultiplier_canonical line 71
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_canonical line 80
6. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeHeatBoost_canonical line 86
7. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.heatEvaluation_eq line 98
8. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.heatEvaluationVector_eq line 102
9. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.heatInnerKernel_eq line 107
10. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.heatRegularize_eq line 111
11. def OAI.TamingCompatibility.GeometricHilbert.unitSymbol line 131
12. lemma OAI.TamingCompatibility.GeometricHilbert.unitSymbol_bound line 132
13. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeResolvent_unit_spectral line 136
14. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeResolvent_rate_repr line 147
15. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_inner_series line 182
16. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeHeatMultiplier_hasDerivAt line 194
17. lemma OAI.TamingCompatibility.GeometricHilbert.heatScalarSeries_hasDerivAt line 212
18. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_resolvent_hasDerivAt line 241
19. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_smooth_hasDerivAt line 264
20. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSpectralHeat_weak_hasDerivAt line 279
21. lemma OAI.TamingCompatibility.GeometricHilbert.WeakHeat.integral_eq_of_dense_weak line 312
22. lemma OAI.TamingCompatibility.GeometricHilbert.WeakHeat.hasDerivAt_of_dense_weak line 335
23. lemma OAI.TamingCompatibility.GeometricHilbert.WeakHeat.zero_of_resolvent_weak line 354
24. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeResolvent_energy_le line 418
25. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeResolvent_smooth_core line 432
26. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeWeakHeat_zero line 451
27. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeWeakHeat_eq_spectral line 471