OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorDerivative.lean

GitHub source file

4 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. def OAI.LipschitzHilbert.SourceLatticePacket.boundedSelectedTopSum line 17
  2. theorem OAI.LipschitzHilbert.SourceLatticePacket.boundedSelectedTopSum_horizontal_bound line 25
  3. theorem OAI.LipschitzHilbert.SourceLatticePacket.source_bounded_coefficient_derivative line 72
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_selector_top_derivative line 123