OAI/Analysis/LipschitzHilbert/Trees/SourceShearedEnvelopeEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The weighted envelope estimate in the physical coordinates of an arbitrary reference slope. The shear preserves product Lebesgue measure.

  1. def OAI.LipschitzHilbert.shearedTileEnvelope line 15
  2. def OAI.LipschitzHilbert.shearedTopReciprocal line 18
  3. theorem OAI.LipschitzHilbert.coordinateBox_shear line 21
  4. theorem OAI.LipschitzHilbert.sheared_packed_envelope_energy line 30