OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationErrorRaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

High-order carrier-free decay and the actual top geometry survive snapping the translated labeled lattice. These are the raw hypotheses used in the weighted angular-error concentration theorem.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_absolute_snapped_order line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_absolute_snapped_decay line 35
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.snapped_top_horizontal line 45
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.snapped_top_vertical line 56