OAI/Analysis/KLS/Sobolev/WholeSpace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeGiorgi.C_gns line 16
  2. theorem OAI.DeGiorgi.C_gns_nonneg line 20
  3. lemma OAI.DeGiorgi.sobolev_exp_pos line 23
  4. lemma OAI.DeGiorgi.sobolev_exponent_relation line 29
  5. lemma OAI.DeGiorgi.sobolev_exponent_nnreal_relation line 37
  6. theorem OAI.DeGiorgi.sobolev_smooth line 47
  7. theorem OAI.DeGiorgi.norm_fderiv_eq_norm_partials line 80
  8. theorem OAI.DeGiorgi.aestronglyMeasurable_euclidean_of_components line 111
  9. theorem OAI.DeGiorgi.tendstoInMeasure_of_eLpNorm_tendsto line 127
  10. theorem OAI.DeGiorgi.partialDiff_aestronglyMeasurable line 136
  11. theorem OAI.DeGiorgi.partialDiff_sum_tendsto_zero line 149
  12. theorem OAI.DeGiorgi.gradVec_eLpNorm_le_sum line 176
  13. theorem OAI.DeGiorgi.sobolev_of_approx line 251