OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedErrorRaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original selector concentration with packetwise length control. Empty initial scales impose no global top-length assumption; constants are unchanged.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.snapped_supported_top_horizontal line 18
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.snapped_supported_top_vertical line 29