OAI/Geometry/Riemannian/HarmonicCore/WeakLimits.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.bounded_family_test_limit line 12
  2. def OAI.HarmonicCounterexample.Main.SmoothMetric3.HasWeakDirectionalDerivative line 32
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.test_finiteDifference_tendsto line 36
  4. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.bounded_finiteDifference_has_weakDerivative line 42
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_scalar_lipschitz line 59
  6. def OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceScalar line 66
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceScalar_continuous line 69
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceScalar_bound line 74
  9. def OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceScalarCLM line 88
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceScalarCLM_coe line 94
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceScalarCLM_norm line 101
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifference_scalar_product line 108
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifference_cutoff_bound line 133
  14. def OAI.HarmonicCounterexample.Main.SmoothMetric3.componentL2 line 143
  15. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.componentL2_coe line 146
  16. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.componentL2_norm line 150
  17. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.componentL2_translate line 157
  18. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.componentL2_finiteDifference line 165
  19. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_interior_secondDerivative line 169