OAI/Analysis/LipschitzHilbert/Trees/SourceTopGood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The joint top-sum and covariant-derivative bound of §5, including a common physical-plane exception and a threshold fixed before the family.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.source_top_good line 14