OAI/Analysis/LipschitzHilbert/Packets/PacketDataParentFullResidual.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A parent-cone reference event controls the original short residuals. The remaining long packets occur only in the terminal block and retain the original single-scale selector estimate.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_physical_parent_full_residual_square line 17