OAI/Analysis/LipschitzHilbert/Phase/SourcePathPrediction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The residual-free predictor on the actual packet path. Its child family and coefficients are the same ones used by the physical estimate.

  1. def OAI.LipschitzHilbert.AngularGrid.sourceBlockPrediction line 15
  2. def OAI.LipschitzHilbert.AngularGrid.sourceShiftedPathPrediction line 29
  3. theorem OAI.LipschitzHilbert.AngularGrid.sourceBlockPrediction_measurable line 38
  4. theorem OAI.LipschitzHilbert.AngularGrid.sourceShiftedPathPrediction_measurable line 58
  5. theorem OAI.LipschitzHilbert.AngularGrid.sourceShiftedPathPrediction_pos line 71