OAI/Geometry/Perimeter/Regularity/HasC1TraceAt.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RPI.Boundary.HasC1TraceAt line 13
2. theorem OAI.RPI.Boundary.exists_c1_eqOn_of_local_trace line 18
3. def OAI.RPI.Boundary.HasC1TraceJetAt line 50
4. lemma OAI.RPI.Boundary.HasC1TraceJetAt.trace line 55
5. theorem OAI.RPI.Boundary.exists_c1_cutoff_trace line 61
6. lemma OAI.RPI.Boundary.surfaceGradient_norm_le_fderiv line 117
7. lemma OAI.RPI.Boundary.c1Mollify_surfaceGradient_tendsto line 123
8. lemma OAI.RPI.Boundary.c1_surfaceGradient_aestronglyMeasurable line 132
9. lemma OAI.RPI.Boundary.c1Mollify_pair_bounded line 141
10. lemma OAI.RPI.bounded_tendsto_toLp_two line 168
11. theorem OAI.RPI.Boundary.c1_compact_mem_sobolevGraph line 210
12. theorem OAI.RPI.Boundary.exists_c1_compact_trace_on_bounded line 238
13. theorem OAI.RPI.Boundary.c1_mem_sobolevGraph_bounded line 263
14. theorem OAI.RPI.Boundary.c1_capacity_trace_mem_sobolevGraph line 294
15. theorem OAI.RPI.Boundary.HasC1TraceJetAt.comp line 348
16. theorem OAI.RPI.Boundary.HasC1TraceJetAt.smoothTruncation line 360
17. theorem OAI.RPI.Boundary.c1_surfaceGradient_memLp_on_ball line 369
18. theorem OAI.RPI.Boundary.c1_exists_smooth_representative_near_regular_test line 403
19. theorem OAI.RPI.Boundary.c1_surfaceGradient_memLp_of_compact line 447
20. theorem OAI.RPI.Boundary.c1_regular_gradient_memLp_indicator_test line 470
21. theorem OAI.RPI.Boundary.c1_integrable_regular_test_pair line 492