OAI/Geometry/Riemannian/HarmonicCore/DirectionLimits.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.component_testDerivative line 13
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.testGraph_snd line 24
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.derivative_test_approximation line 27
  4. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_finiteDifference_tendsto line 39
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.forcing_finiteDifference_tendsto line 70
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_operator_taylor_bound line 82
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientDirection_continuous line 94
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientDirection_bound line 98
  9. def OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientDirectionCLM line 106
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceCoefficient_taylor_bound line 113
  11. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceCoefficientCLM_tendsto line 129
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.shiftedCoefficientCLM_tendsto line 150
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.shiftedCoefficientCLM_tendsto_apply line 169
  14. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_direction_graph line 188
  15. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_direction_equation line 210