OAI/Geometry/RCD/Sobolev/BochnerSquareSaturation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The scalar dimensional inequality excludes an extra orthogonal square

The vectors in this calculation represent centered squares of regular test functions. Their sources and mixed Bochner densities are the exact quantities computed by the local product rules.

  1. theorem OAI.RegularPointCoordinates.dimensional_square_residual_zero line 16
  2. theorem OAI.RegularPointCoordinates.bochner_square_saturation line 25