OAI/Analysis/LipschitzHilbert/Packets/PacketDataIntrinsicReverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reverse disparity with the intrinsic profile budget. The auxiliary jet parameters are reset before the estimate, and the literal physical form is transported back unchanged.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_intrinsic_cross_reverse_disparity line 14