OAI/Geometry/Perimeter/Regularity/RegularSupersolutionC1Test.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPI.Boundary.regular_supersolution_c1_test line 13
2. theorem OAI.RPI.Boundary.c1_hausdorff_trace_mem_sobolevGraph line 91
3. theorem OAI.RPI.Boundary.HasC1TraceJetAt.mul_smooth line 115
4. theorem OAI.RPI.Boundary.c1_regular_trace_jet_mul_spatial line 129
5. theorem OAI.RPI.Boundary.c1_hausdorff_trace_mem_sobolevGraph_ball line 152
6. theorem OAI.RPI.Boundary.c1_trace_aestronglyMeasurable_of_singular_dim line 212
7. theorem OAI.RPI.Boundary.c1_min_one_mem_sobolevGraph_ball line 236
8. theorem OAI.RPI.Boundary.c1_smoothTruncation_regular_test line 287
9. theorem OAI.RPI.Boundary.c1_regular_gradient_memLp_test line 356
10. theorem OAI.RPI.Boundary.c1_smoothTruncation_regular_energy line 378