OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledResidualThreshold.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On the actual good-reference event, the residual-square expression has a single fixed polynomial bound. The error and main quantities are the original physical packet sums, not abstract envelope assumptions.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_residual_expression_polynomial line 18
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_packet_residual_square_polynomial line 51