OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedSelectorDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The horizontal derivative estimate uses the coefficient norm bound for the original smooth selector. It supplies the horizontal term in the motion and prediction estimates.

  1. theorem OAI.LipschitzHilbert.SourceLatticePacket.boundedSelectedTopSum_horizontal_bound_of_supported line 20
  2. theorem OAI.LipschitzHilbert.SourceLatticePacket.source_bounded_coefficient_derivative_of_supported line 67
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_selector_top_derivative_of_supported line 118