OAI/MeasureTheory/Falconer/Estimates/LaplacianIsometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rotation invariance and locality of the actual quadratic jets

These are identities for the Euclidean derivatives in the published input. They allow the choice of tangent orthonormal coordinates and fixed cutoffs to be removed from the resulting stationary coefficients.

  1. theorem OAI.Falconer.euclidean_laplacian_isometry line 17
  2. theorem OAI.Falconer.euclidean_iterated_laplacian_isometry line 37
  3. theorem OAI.Falconer.quadraticJetCoefficient_isometry line 47
  4. theorem OAI.Falconer.euclidean_iterated_laplacian_congr line 53
  5. theorem OAI.Falconer.quadraticJetCoefficient_congr line 63