OAI/Geometry/Perimeter/Regularity/SurfaceGradientComp.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPI.Boundary.surfaceGradient_comp line 13
2. theorem OAI.RPI.Boundary.HasSmoothTraceJetAt.comp line 23
3. def OAI.RPI.Boundary.truncatedGradient line 35
4. theorem OAI.RPI.Boundary.truncationSlope_smul_truncatedGradient line 38
5. theorem OAI.RPI.Boundary.HasSmoothTraceJetAt.smoothTruncation line 46
6. theorem OAI.RPI.Boundary.smoothTruncation_norm_le line 67
7. theorem OAI.RPI.Boundary.truncationSlope_norm_le line 72
8. theorem OAI.RPI.Boundary.min_one_memLp line 76
9. theorem OAI.RPI.Boundary.smoothTruncation_memLp line 85
10. theorem OAI.RPI.Boundary.truncationGradient_memLp line 91
11. theorem OAI.RPI.Boundary.smoothTruncation_error_energy_tendsto line 103
12. theorem OAI.RPI.Boundary.truncationGradient_error_energy_tendsto line 136
13. theorem OAI.RPI.Boundary.smoothTruncation_pair_tendsto line 176
14. theorem OAI.RPI.Boundary.surfaceGradient_eq_tangentialGradient_filled line 214
15. theorem OAI.RPI.Boundary.surfaceGradient_ae_eq_tangentialGradient_filled line 245
16. theorem OAI.RPISingularHarnack.wholeBoundarySobolev_of_local_sobolevGraph_filled line 273
17. theorem OAI.RPI.Boundary.HasSmoothTraceJetAt.mul_smooth line 332
18. theorem OAI.RPI.Boundary.regular_trace_jet_mul_spatial line 346
19. theorem OAI.RPI.Boundary.hausdorff_trace_mem_sobolevGraph_ball line 369
20. theorem OAI.RPI.Boundary.trace_aestronglyMeasurable_of_singular_dim line 439
21. theorem OAI.RPI.Boundary.min_one_mem_sobolevGraph_ball line 463