OAI/Geometry/TamingCompatibility/HeatFlow/FlatHeat.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.GeometricHilbert.FlatHeat.V line 9
2. def OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat line 11
3. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_pos line 14
4. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_nonneg line 18
5. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_neg line 22
6. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_continuous line 25
7. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.gaussian_integrable line 29
8. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.gaussian_integral line 35
9. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_integrable line 42
10. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_integral line 50
11. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_scale line 59
12. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_diagonal line 66
13. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_contDiff line 69
14. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_hasFDerivAt line 72
15. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_fderiv line 82
16. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_hasDerivAt_time line 87
17. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_directional_hasFDerivAt line 101
18. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_hessian line 122
19. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.gaussian_complete_square line 130
20. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_product line 142
21. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_convolution_integrable line 163
22. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_convolution line 168
23. def OAI.TamingCompatibility.GeometricHilbert.FlatHeat.laplacian line 173
24. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_equation line 177
25. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.gaussian_weight_absorption line 187
26. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_gradient_bound line 218
27. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.heat_hessian_bound line 228
28. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.normal_jet_gradient_bound line 250
29. lemma OAI.TamingCompatibility.GeometricHilbert.FlatHeat.normal_jet_hessian_bound line 262