OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorMotion.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 line 15
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_selector_masked_interval_motion line 89
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_selector_predictable_masked_interval_motion line 161