OAI/Geometry/Perimeter/Regularity/IntegralInnerEqInnerToLp.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPI.integral_inner_eq_inner_toLp line 18
  2. theorem OAI.RPI.integrable_inner_of_memLp line 26
  3. theorem OAI.RPI.tendsto_integral_inner_of_L2_zero line 33
  4. theorem OAI.RPI.energy_inequality_of_capacity_cutoffs line 47
  5. theorem OAI.RPI.Boundary.surfaceGradient_memLp_on_ball line 104
  6. theorem OAI.RPI.Boundary.surfaceGradient_eq_zero_of_notMem_tsupport line 126
  7. theorem OAI.RPI.Boundary.tsupport_mul_disjoint_Singular line 132
  8. theorem OAI.RPI.Boundary.full_test_of_regular_tests line 145
  9. theorem OAI.RPI.Boundary.exists_smooth_representative_near_regular_test line 227
  10. theorem OAI.RPI.Boundary.surfaceGradient_memLp_of_compact line 271
  11. theorem OAI.RPI.Boundary.regular_gradient_memLp_indicator_test line 294
  12. theorem OAI.RPI.Boundary.integrable_regular_test_pair line 316
  13. theorem OAI.RPI.Boundary.smoothTruncation_regular_test line 331