OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedSelectorIntervalMotion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Carrier and top-mask motion for the original smooth-selector coefficients. The snapshot concentration premise remains the original one; the horizontal derivative is proved from the original packets.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_selector_interval_motion_of_supported line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_selector_masked_interval_motion_of_supported line 90
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_selector_predictable_masked_interval_motion_of_supported line 162