OAI/Analysis/LipschitzHilbert/Phase/SourcePredictionIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The marked-factor integral for unequal source blocks. The error is paid through its path sum; all averaging remains on the original nested line grid.

  1. theorem OAI.LipschitzHilbert.source_skipped_path_integral line 14