OAI/Analysis/CircleDomains/Sobolev/PlanarGradientDensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The planar gradient density used in line payment

The two Euclidean components are the real derivative on 1 and I. The horizontal line derivative is the first component, and the square of the density is the ordinary Euclidean Dirichlet energy integrand.

  1. def OAI.CircleDomainRigidity.horizontalLine line 22
  2. theorem OAI.CircleDomainRigidity.continuous_horizontalLine line 24
  3. theorem OAI.CircleDomainRigidity.contDiff_horizontalLine line 27
  4. theorem OAI.CircleDomainRigidity.hasDerivAt_horizontalLine line 30
  5. def OAI.CircleDomainRigidity.euclideanGradientEnergy line 34
  6. def OAI.CircleDomainRigidity.euclideanGradientNorm line 37
  7. theorem OAI.CircleDomainRigidity.euclideanGradientEnergy_nonneg line 40
  8. theorem OAI.CircleDomainRigidity.euclideanGradientNorm_sq line 43
  9. theorem OAI.CircleDomainRigidity.measurable_euclideanGradientNorm line 47
  10. theorem OAI.CircleDomainRigidity.memLp_indicator_euclideanGradientNorm line 51
  11. theorem OAI.CircleDomainRigidity.horizontal_derivative_le_gradient line 62
  12. theorem OAI.CircleDomainRigidity.horizontal_cluster_is_planar line 70