OAI/Geometry/Perimeter/Regularity/RawConeLink.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RPISingularHarnack.SphericalFrankel.End line 12
2. def OAI.RPISingularHarnack.SphericalFrankel.linTrace line 14
3. def OAI.RPISingularHarnack.SphericalFrankel.linkTrace line 18
4. def OAI.RPISingularHarnack.SphericalFrankel.projMap line 21
5. lemma OAI.RPISingularHarnack.SphericalFrankel.projMap_apply line 25
6. lemma OAI.RPISingularHarnack.SphericalFrankel.linTrace_sub line 28
7. lemma OAI.RPISingularHarnack.SphericalFrankel.linTrace_add line 33
8. lemma OAI.RPISingularHarnack.SphericalFrankel.linTrace_smul line 38
9. lemma OAI.RPISingularHarnack.SphericalFrankel.linTrace_id line 43
10. lemma OAI.RPISingularHarnack.SphericalFrankel.linTrace_rank line 46
11. lemma OAI.RPISingularHarnack.SphericalFrankel.linkTrace_sub line 52
12. lemma OAI.RPISingularHarnack.SphericalFrankel.linkTrace_add line 57
13. lemma OAI.RPISingularHarnack.SphericalFrankel.linkTrace_smul line 62
14. lemma OAI.RPISingularHarnack.SphericalFrankel.linkTrace_rank line 68
15. lemma OAI.RPISingularHarnack.SphericalFrankel.proj_self_left line 75
16. lemma OAI.RPISingularHarnack.SphericalFrankel.proj_self_right line 80
17. lemma OAI.RPISingularHarnack.SphericalFrankel.inner_proj_swap line 84
18. lemma OAI.RPISingularHarnack.SphericalFrankel.inner_proj_self line 91
19. lemma OAI.RPISingularHarnack.SphericalFrankel.linkTrace_id line 97
20. lemma OAI.RPISingularHarnack.SphericalFrankel.linkTrace_proj line 102
21. def OAI.RPISingularHarnack.SphericalFrankel.linkDiv line 110
22. lemma OAI.RPISingularHarnack.SphericalFrankel.linkDiv_scalar_constant line 113
23. lemma OAI.RPISingularHarnack.SphericalFrankel.linkDiv_scalar_proj line 133
24. lemma OAI.RPISingularHarnack.SphericalFrankel.linTrace_rank_general line 161
25. def OAI.RPISingularHarnack.SphericalFrankel.sphereProj line 173
26. def OAI.RPISingularHarnack.SphericalFrankel.planeTrace line 176
27. lemma OAI.RPISingularHarnack.SphericalFrankel.planeTrace_add line 179
28. lemma OAI.RPISingularHarnack.SphericalFrankel.planeTrace_sub line 184
29. lemma OAI.RPISingularHarnack.SphericalFrankel.planeTrace_smul line 189
30. lemma OAI.RPISingularHarnack.SphericalFrankel.planeTrace_rank line 194
31. lemma OAI.RPISingularHarnack.SphericalFrankel.planeTrace_comp_sphereProj line 199
32. lemma OAI.RPISingularHarnack.SphericalFrankel.sphereProj_self line 208
33. lemma OAI.RPISingularHarnack.SphericalFrankel.planeTrace_sphereProj line 211
34. def OAI.RPISingularHarnack.SphericalFrankel.radialUnit line 216
35. lemma OAI.RPISingularHarnack.SphericalFrankel.radialUnit_norm line 218
36. lemma OAI.RPISingularHarnack.SphericalFrankel.radialUnit_scale line 221
37. lemma OAI.RPISingularHarnack.SphericalFrankel.radialUnit_contDiffAt line 224
38. lemma OAI.RPISingularHarnack.SphericalFrankel.radialUnit_measurable line 228
39. lemma OAI.RPISingularHarnack.SphericalFrankel.radialUnit_hasFDerivAt line 231
40. def OAI.RPISingularHarnack.SphericalFrankel.sphereLift line 253
41. lemma OAI.RPISingularHarnack.SphericalFrankel.inner_radialUnit_sphereLift line 256
42. lemma OAI.RPISingularHarnack.SphericalFrankel.sphereLift_contDiffAt line 260
43. lemma OAI.RPISingularHarnack.SphericalFrankel.planeTrace_sphereLift line 267
44. def OAI.RPISingularHarnack.SphericalFrankel.annularProfile line 299
45. def OAI.RPISingularHarnack.SphericalFrankel.annularCut line 301
46. lemma OAI.RPISingularHarnack.SphericalFrankel.annularProfile_contDiff line 303
47. lemma OAI.RPISingularHarnack.SphericalFrankel.annularCut_contDiff line 307
48. lemma OAI.RPISingularHarnack.SphericalFrankel.annularCut_nonneg line 310
49. lemma OAI.RPISingularHarnack.SphericalFrankel.annularCut_eq_zero_inner line 313
50. lemma OAI.RPISingularHarnack.SphericalFrankel.annularCut_eq_zero_outer line 318
51. lemma OAI.RPISingularHarnack.SphericalFrankel.annularCut_pos line 323
52. lemma OAI.RPISingularHarnack.SphericalFrankel.annularCut_hasFDerivAt line 329
53. def OAI.RPISingularHarnack.SphericalFrankel.annularLift line 339
54. lemma OAI.RPISingularHarnack.SphericalFrankel.annularLift_contDiff line 342
55. lemma OAI.RPISingularHarnack.SphericalFrankel.annularLift_tsupport line 354
56. lemma OAI.RPISingularHarnack.SphericalFrankel.planeTrace_annularLift line 362
57. lemma OAI.RPISingularHarnack.SphericalFrankel.annularLift_zero_nhds line 383
58. def OAI.RPISingularHarnack.SphericalFrankel.annularWeight line 389
59. lemma OAI.RPISingularHarnack.SphericalFrankel.annularWeight_nonneg line 391
60. lemma OAI.RPISingularHarnack.SphericalFrankel.annularWeight_continuous line 394
61. lemma OAI.RPISingularHarnack.SphericalFrankel.annularWeight_tsupport line 406
62. def OAI.RPISingularHarnack.SphericalFrankel.annularWeightNN line 414
63. lemma OAI.RPISingularHarnack.SphericalFrankel.annularWeightNN_measurable line 416
64. def OAI.RPISingularHarnack.SphericalFrankel.annularFrameMeasure line 419
65. def OAI.RPISingularHarnack.SphericalFrankel.frameOf line 423
66. lemma OAI.RPISingularHarnack.SphericalFrankel.frameOf_measurable line 426
67. def OAI.RPISingularHarnack.SphericalFrankel.annularLink line 429
68. lemma OAI.RPISingularHarnack.SphericalFrankel.annularFrameMeasure_finite line 432
69. lemma OAI.RPISingularHarnack.SphericalFrankel.annularLink_finite line 448
70. lemma OAI.RPISingularHarnack.SphericalFrankel.annularLink_frames line 453
71. lemma OAI.RPISingularHarnack.SphericalFrankel.linkDiv_continuous line 471
72. structure OAI.RPISingularHarnack.SphericalFrankel.LinkStationary line 477
73. lemma OAI.RPISingularHarnack.SphericalFrankel.annularLink_stationary line 480