OAI/MeasureTheory/Falconer/Measures/SpatialRestriction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Measurable product restrictions stay in the original endpoint jet class

  1. theorem OAI.Falconer.endpointTransform_restrict_indicator line 10
  2. def OAI.Falconer.DescriptorJetSymbol.restrictSpatial line 24
  3. theorem OAI.Falconer.DescriptorJetSymbol.restrictSpatial_endpoint line 30