OAI/Analysis/LipschitzHilbert/Packets/SourceBoundaryPacketError.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Boundary coefficient deficits acting on the original stopping bands. The bound uses their raw prefix sums, with no loss in the number of levels.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundaryCoefficient_bounds line 16
  2. theorem OAI.LipschitzHilbert.AngularGrid.measurable_sourceBoundaryLogLoss_withOrigin line 31
  3. theorem OAI.LipschitzHilbert.AngularGrid.measurable_sourceBoundaryCoefficient_withOrigin line 41
  4. theorem OAI.LipschitzHilbert.AngularGrid.source_boundary_deficit_sum_le_log_loss line 59
  5. theorem OAI.LipschitzHilbert.AngularGrid.source_boundary_expected_packet_error line 85