OAI/Geometry/Riemannian/HarmonicCore/SobolevOrder.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev line 16
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevDerivative_eq_of_value_eq line 21
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.zero line 28
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.lower line 33
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.gradient line 40
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.add line 47
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.smul line 62
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.sum line 72
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_direction_contDiff line 81
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.cutoffSobolev_direction line 85
  11. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.smooth_mul line 106
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.exists_common_graph line 129
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.mono line 139
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.coefficient line 150
  15. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.componentL2_vectorize line 168
  16. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.vector_sum line 176
  17. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarFieldCLM_mul line 183
  18. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_forced_cutoff_restrict line 193