OAI/Analysis/LiebThirring/EnergyAlgebra.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.val_sub line 13
2. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.grad_sub line 14
3. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_tendsto line 16
4. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.eventually_cut_linearIndependent line 37
5. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.val_sum line 41
6. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.grad_sum line 48
7. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.compact_smul line 55
8. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.compact_sum line 58
9. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.compact_of_mem_span line 65
10. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.energy_add_left line 76
11. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.energy_smul_left line 84
12. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.energy_sum_left line 91
13. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.energy_sum_sum line 99
14. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.inner_sum_sum line 114