OAI/Analysis/LipschitzHilbert/Packets/PacketDataModelBilinearRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete low/high density assembly for the actual finite bilinear model in a direction chart. The high family is constructed from the original collection; no energy or counting premise remains.

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