OAI/Analysis/LipschitzHilbert/Packets/PacketDataOriginalParentMarkedPath.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual source cell marks and local original-packet estimates supply the remaining hypotheses of the stopped-path theorem.

  1. def OAI.LipschitzHilbert.PacketLatticeData.originalParentMarkedPathBoundAt line 16
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_original_parent_marked_path_bound line 134