OAI/Analysis/LipschitzHilbert/Phase/SourceSupportedSelectorBlockPredictor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local source predictor for the original physical packet family. Its normalized motion and insignificant-child hypotheses are discharged by the actual packet estimates and the snapshot concentration bounds.

  1. theorem OAI.LipschitzHilbert.AngularGrid.modulation_rescale line 21

    Also declared: OAI/Analysis/LipschitzHilbert/Phase/SourceSelectorBlockPredictor.lean:21 (same declaration text).

  2. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_supported_selector_block_predictor line 28