OAI/Analysis/StrictMeans/DiscreteLaplacian.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.Grid.line_hasDerivAt line 11
  2. lemma OAI.StrictInverseFirstPower.Grid.line_second_hasDerivAt line 18
  3. lemma OAI.StrictInverseFirstPower.Grid.centered_difference_lower line 28
  4. lemma OAI.StrictInverseFirstPower.Grid.second_continuousAt line 58
  5. lemma OAI.StrictInverseFirstPower.Grid.positive_laplace_ascent line 63
  6. lemma OAI.StrictInverseFirstPower.Grid.compact_laplace_ascent line 105