OAI/Analysis/LipschitzHilbert/Packets/PacketDataParentResidualSquare.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The square-reference event is taken on the literal parent cone and in the path-top reference direction. Its good event controls the original short residuals without an equality of reference slopes.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_physical_parent_short_square line 16