OAI/Geometry/SmoothYau/Limits/ManifoldSobolevInclusionCoordinate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.boundedDistribution_memLp line 20
  2. lemma OAI.YauCounterexamples.sobolev_zero_distribution line 28
  3. lemma OAI.YauCounterexamples.sobolev_norm_zero_repr line 35
  4. lemma OAI.YauCounterexamples.compact_L2_bound line 50
  5. lemma OAI.YauCounterexamples.sobolev_zero_compact_bound line 80
  6. lemma OAI.YauCounterexamples.supported_bcf_dist_le line 102
  7. theorem OAI.YauCounterexamples.supported_bcf_subsequence line 118
  8. lemma OAI.YauCounterexamples.sobolev_repr_dist_bound line 156
  9. theorem OAI.YauCounterexamples.sobolev_rellich_subsequence line 168
  10. lemma OAI.YauCounterexamples.manifoldSobolevInclusion_coordinate line 229
  11. theorem OAI.YauCounterexamples.manifoldSobolevInclusion_compact line 243