OAI/Analysis/LiebThirring/CutoffEnergy.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.SobolevProof.c1L2Submodule line 12

   Source documentation

   C¹ representatives of real H¹, with the L² inner product (not the H¹ norm).

   def c1L2Submodule : Submodule ℝ ((ℝ → ℝ) × (ℝ → ℝ)) where
   …

2. def OAI.SharpLiebThirring.SobolevProof.C1L2 line 24
3. instance OAI.SharpLiebThirring.SobolevProof.(instance at line 25) line 25
4. instance OAI.SharpLiebThirring.SobolevProof.(instance at line 26) line 26
5. def OAI.SharpLiebThirring.SobolevProof.C1L2.val line 29
6. def OAI.SharpLiebThirring.SobolevProof.C1L2.grad line 30
7. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.val_memLp line 31
8. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.grad_memLp line 32
9. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.grad_continuous line 33
10. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.hasDerivAt line 34
11. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.continuous line 35
12. def OAI.SharpLiebThirring.SobolevProof.C1L2.toLp line 37
13. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.toLp_injective line 42
14. instance OAI.SharpLiebThirring.SobolevProof.C1L2.(instance at line 52) line 52
15. instance OAI.SharpLiebThirring.SobolevProof.C1L2.(instance at line 53) line 53
16. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.val_zero line 55
17. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.grad_zero line 56
18. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.val_add line 57
19. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.grad_add line 58
20. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.val_smul line 59
21. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.grad_smul line 60
22. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.inner_eq_integral line 62
23. lemma OAI.SharpLiebThirring.SobolevProof.locallyIntegrable_intervalIntegrable line 74
24. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.contDiff line 83
25. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.ac line 88
26. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.deriv_val line 91
27. def OAI.SharpLiebThirring.SobolevProof.C1L2.IsEigen line 94

    Source documentation

    Exact integrated real eigen-equation; no regularity of W beyond local L¹.

    def IsEigen (W : ℝ → ℝ) (k : ℝ) (u : C1L2) : Prop :=
    …

    Mentions: OAI.SharpLiebThirring.SobolevProof.C1L2

28. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.eigen_integrable line 97
29. def OAI.SharpLiebThirring.SobolevProof.C1L2.eigenSubmodule line 101
30. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.IsEigen.grad_ac line 118
31. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.IsEigen.grad_deriv line 127
32. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.IsEigen.weak_interval line 137
33. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.IsEigen.weak_compact line 149
34. lemma OAI.SharpLiebThirring.SobolevProof.cutoffDerivative_compact line 184
35. def OAI.SharpLiebThirring.SobolevProof.C1L2.cut line 191
36. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_val line 202
37. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_grad line 203
38. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_compact line 205
39. def OAI.SharpLiebThirring.SobolevProof.C1L2.cutMap line 207
40. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.integrable_val_mul line 227
41. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.integrable_grad_mul line 229
42. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.integral_real_multiplier_tendsto line 232
43. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cutoff_inner_tendsto line 244
44. def OAI.SharpLiebThirring.SobolevProof.C1L2.energy line 260
45. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.energy_symm line 263
46. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.integrable_potential line 267
47. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_energy_algebra line 271
48. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_error_integrable line 276
49. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_cross_integrable line 285
50. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_weak_integrable line 291
51. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_weak_zero line 297
52. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_energy_identity line 304
53. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.cut_energy_tendsto line 333
54. lemma OAI.SharpLiebThirring.SobolevProof.C1L2.eigen_orthogonal line 354