OAI/Geometry/SmoothYau/Smoothness/ConstantComplexProductJetBound.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.chartLocalize line 25
  2. lemma OAI.YauCounterexamples.chartLocalize_eq line 30
  3. lemma OAI.YauCounterexamples.support_chartLocalize line 34
  4. lemma OAI.YauCounterexamples.isCompact_chartSupport line 46
  5. lemma OAI.YauCounterexamples.hasCompactSupport_chartLocalize line 52
  6. lemma OAI.YauCounterexamples.tsupport_chartLocalize_subset line 59
  7. lemma OAI.YauCounterexamples.contDiff_chartLocalize line 67
  8. def OAI.YauCounterexamples.chartSchwartz line 87
  9. lemma OAI.YauCounterexamples.chartSchwartz_apply line 95
  10. abbrev OAI.YauCounterexamples.ManifoldSmoothFunctions line 125
  11. def OAI.YauCounterexamples.smoothToBounded line 129
  12. def OAI.YauCounterexamples.chartSchwartzLinear line 134
  13. def OAI.YauCounterexamples.atlasSobolevLocalization line 157
  14. def OAI.YauCounterexamples.manifoldSobolevSubmodule line 163
  15. abbrev OAI.YauCounterexamples.ManifoldSobolev line 166
  16. instance OAI.YauCounterexamples.manifoldSobolev_completeSpace line 168
  17. def OAI.YauCounterexamples.smoothToManifoldSobolev line 172
  18. lemma OAI.YauCounterexamples.denseRange_smoothToManifoldSobolev line 178
  19. lemma OAI.YauCounterexamples.manifold_sobolev_sup_bound line 212
  20. def OAI.YauCounterexamples.manifoldSobolevRepresentative line 249
  21. lemma OAI.YauCounterexamples.manifoldSobolevRepresentative_smooth line 253
  22. def OAI.YauCounterexamples.chartLift line 278
  23. lemma OAI.YauCounterexamples.contMDiff_chartLift line 281
  24. lemma OAI.YauCounterexamples.tsupport_chartLocalize_image line 294
  25. lemma OAI.YauCounterexamples.contDiffOn_chartTransition line 302
  26. lemma OAI.YauCounterexamples.chart_overlap_cutoff_support line 312
  27. lemma OAI.YauCounterexamples.chartLocalize_chartLift line 327
  28. lemma OAI.YauCounterexamples.norm_smoothToManifoldSobolev_mono line 357
  29. def OAI.YauCounterexamples.manifoldSobolevInclusion line 368
  30. lemma OAI.YauCounterexamples.manifoldSobolevInclusion_smooth line 374
  31. lemma OAI.YauCounterexamples.norm_manifoldSobolevInclusion_le line 384
  32. lemma OAI.YauCounterexamples.manifoldSobolevInclusion_representative line 391
  33. lemma OAI.YauCounterexamples.constant_complex_product_jet_bound line 432
  34. theorem OAI.YauCounterexamples.localized_real_chart_jet_bound line 460