OAI/Analysis/KLS/Sobolev/SobolevApproximation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DeGiorgi.exists_smooth_cutoff line 17
  2. lemma OAI.DeGiorgi.memW01p_of_global_approx_supported line 48
  3. theorem OAI.DeGiorgi.zero_outside_of_tsupport_subset line 67
  4. theorem OAI.DeGiorgi.fderiv_apply_zero_outside_of_tsupport_subset line 76
  5. def OAI.DeGiorgi.zeroExtend_memW1pWitness_p line 89
  6. lemma OAI.DeGiorgi.tsupport_convolution_subset_cthickening line 264
  7. lemma OAI.DeGiorgi.tsupport_normed_convolution_subset_cthickening line 289
  8. def OAI.DeGiorgi.shrinkingBump line 299
  9. lemma OAI.DeGiorgi.tendsto_shrinkingBump_rOut line 308
  10. theorem OAI.DeGiorgi.eLpNorm_normedConvolution_le line 316
  11. theorem OAI.DeGiorgi.normedConvolution_sub_eq line 476
  12. theorem OAI.DeGiorgi.eLpNorm_normedConvolution_sub_le line 504
  13. theorem OAI.DeGiorgi.tendsto_eLpNorm_normedConvolution_sub_of_continuous line 523
  14. theorem OAI.DeGiorgi.tendsto_eLpNorm_normedConvolution_sub line 668
  15. theorem OAI.DeGiorgi.MemW1pWitness.ae_eq_p line 911
  16. theorem OAI.DeGiorgi.MemW1pWitness.ae_eq line 929
  17. theorem OAI.DeGiorgi.convolution_fderiv_eq_convolution_weakPartial_univ line 948
  18. theorem OAI.DeGiorgi.exists_smooth_compactSupport_W1p_approx_univ line 1024
  19. lemma OAI.DeGiorgi.fderiv_apply_eq_zero_of_eq_one_on_cthickening line 1172
  20. theorem OAI.DeGiorgi.tsupport_mul_smooth_bounded_p_weakGrad_component_subset line 1194
  21. theorem OAI.DeGiorgi.exists_smooth_W1p_approx_of_supportedWitness line 1224
  22. theorem OAI.DeGiorgi.memW01p_of_memW1p_of_tsupport_subset line 1426
  23. theorem OAI.DeGiorgi.sobolev_of_memW01p_univ line 1491