OAI/Geometry/Riemannian/HarmonicCore/SobolevComposition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientCLM_tendsto_ae line 16
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_smooth_scalar_comp line 71
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientCLM_tendsto_joint line 80
  4. def OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarDerivativeField line 99
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarDerivativeField_measurable line 102
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarDerivativeField_bound line 106
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_smooth_composition line 111
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.tsupport_comp_add_subset line 190
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_affine_smooth_composition line 199