OAI/Geometry/TamingCompatibility/HeatFlow/VariationalResolvent.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.Fredholm.nullspace line 13
2. lemma OAI.TamingCompatibility.Fredholm.mem_nullspace line 16
3. instance OAI.TamingCompatibility.Fredholm.(instance at line 20) line 20
4. instance OAI.TamingCompatibility.Fredholm.(instance at line 22) line 22
5. lemma OAI.TamingCompatibility.Fredholm.map_orthogonal_nullspace line 26
6. theorem OAI.TamingCompatibility.Fredholm.finiteDimensional_nullspace line 38
7. theorem OAI.TamingCompatibility.Fredholm.exists_inverse_on_complement line 50
8. theorem OAI.TamingCompatibility.Fredholm.exists_generalized_inverse line 84
9. def OAI.TamingCompatibility.Variational.energy line 149
10. lemma OAI.TamingCompatibility.Variational.energy_apply line 153
11. def OAI.TamingCompatibility.Variational.weakSolution line 156
12. lemma OAI.TamingCompatibility.Variational.weakSolution_identity line 160
13. def OAI.TamingCompatibility.Variational.resolvent line 168
14. lemma OAI.TamingCompatibility.Variational.resolvent_compact line 171
15. lemma OAI.TamingCompatibility.Variational.resolvent_symmetric line 175
16. lemma OAI.TamingCompatibility.Variational.resolvent_nonnegative line 187
17. lemma OAI.TamingCompatibility.Variational.resolvent_norm_le line 193
18. lemma OAI.TamingCompatibility.Variational.mem_nullspace_iff line 205
19. theorem OAI.TamingCompatibility.Variational.exists_energy_inverse line 228