OAI/Analysis/NodalLength/ProfileTests.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SharpNodal.Profiles.WeightedProfileBounds line 20
2. lemma OAI.SharpNodal.Profiles.upperSemicontinuousOn_add_real line 31
3. lemma OAI.SharpNodal.Profiles.compact_strict_gap line 38
4. theorem OAI.SharpNodal.Profiles.strict_contact_mass_contradiction line 47
5. theorem OAI.SharpNodal.Profiles.laplacian_nonneg_of_strict_contact line 78
6. def OAI.SharpNodal.Profiles.radiusSquare line 120
7. def OAI.SharpNodal.Profiles.contactQuartic line 122
8. lemma OAI.SharpNodal.Profiles.smooth_radiusSquare line 124
9. lemma OAI.SharpNodal.Profiles.radiusSquare_self line 127
10. lemma OAI.SharpNodal.Profiles.radiusSquare_pos line 129
11. lemma OAI.SharpNodal.Profiles.radiusSquare_partial_self line 132
12. lemma OAI.SharpNodal.Profiles.smooth_contactQuartic line 139
13. lemma OAI.SharpNodal.Profiles.contactQuartic_self line 142
14. lemma OAI.SharpNodal.Profiles.contactQuartic_pos line 145
15. lemma OAI.SharpNodal.Profiles.contactQuartic_partial_self line 148
16. lemma OAI.SharpNodal.Profiles.contactQuartic_laplacian_self line 154
17. lemma OAI.SharpNodal.Profiles.laplacian_add line 160
18. lemma OAI.SharpNodal.Profiles.strictify_gradient line 170
19. lemma OAI.SharpNodal.Profiles.strictify_laplacian line 176
20. lemma OAI.SharpNodal.Profiles.strictify_contact line 180
21. lemma OAI.SharpNodal.Profiles.strictify_strict line 186
22. theorem OAI.SharpNodal.Profiles.smooth_extension_near line 195
23. abbrev OAI.SharpNodal.Profiles.BilinearForm line 215
24. def OAI.SharpNodal.Profiles.SymmetricForm line 217
25. def OAI.SharpNodal.Profiles.centeredQuadratic line 219
26. lemma OAI.SharpNodal.Profiles.smooth_centeredQuadratic line 222
27. lemma OAI.SharpNodal.Profiles.hasFDerivAt_centeredQuadratic line 227
28. lemma OAI.SharpNodal.Profiles.fderiv_centeredQuadratic line 240
29. lemma OAI.SharpNodal.Profiles.partial_centeredQuadratic line 244
30. lemma OAI.SharpNodal.Profiles.partial2_centeredQuadratic line 249
31. lemma OAI.SharpNodal.Profiles.laplacian_centeredQuadratic line 261
32. lemma OAI.SharpNodal.Profiles.symmetric_hessian line 266
33. lemma OAI.SharpNodal.Profiles.hessian_on_basis line 273
34. def OAI.SharpNodal.Profiles.secondTaylorPolynomial line 282
35. lemma OAI.SharpNodal.Profiles.smooth_secondTaylorPolynomial line 285
36. lemma OAI.SharpNodal.Profiles.secondTaylorPolynomial_self line 290
37. lemma OAI.SharpNodal.Profiles.hasFDerivAt_secondTaylorPolynomial line 294
38. theorem OAI.SharpNodal.Profiles.secondTaylorPolynomial_remainder line 301
39. def OAI.SharpNodal.Profiles.IsUpperTest line 323
40. def OAI.SharpNodal.Profiles.NonexceptionalTestProperty line 326
41. def OAI.SharpNodal.Profiles.FullTestProperty line 330
42. def OAI.SharpNodal.Profiles.formTrace line 334
43. def OAI.SharpNodal.Profiles.quadraticAffine line 337
44. lemma OAI.SharpNodal.Profiles.smooth_quadraticAffine line 340
45. lemma OAI.SharpNodal.Profiles.partial_clm_shift line 345
46. lemma OAI.SharpNodal.Profiles.partial_quadraticAffine line 351
47. lemma OAI.SharpNodal.Profiles.laplacian_quadraticAffine line 362
48. lemma OAI.SharpNodal.Profiles.quadraticAffine_self line 374
49. def OAI.SharpNodal.Profiles.innerForm line 377
50. lemma OAI.SharpNodal.Profiles.innerForm_apply line 379
51. lemma OAI.SharpNodal.Profiles.symmetric_innerForm line 381
52. lemma OAI.SharpNodal.Profiles.formTrace_innerForm line 385
53. lemma OAI.SharpNodal.Profiles.formTrace_add line 388
54. lemma OAI.SharpNodal.Profiles.formTrace_smul line 391
55. lemma OAI.SharpNodal.Profiles.formTrace_hessian line 394
56. lemma OAI.SharpNodal.Profiles.centeredQuadratic_add line 398
57. lemma OAI.SharpNodal.Profiles.centeredQuadratic_inner_smul line 402
58. theorem OAI.SharpNodal.Profiles.exists_strict_quadratic_test line 408