OAI/Analysis/LipschitzHilbert/Estimates/ShortTransformMeasurable.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial measurability for positive inner cutoffs and the symmetric principal value. Continuity of the direction field suffices; its value is frozen at each output point throughout the time integration.

  1. theorem OAI.LipschitzHilbert.shortTransform_continuous line 16
  2. theorem OAI.LipschitzHilbert.smoothPrincipalValue_measurable line 45