OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledNarrowTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Main reference tails use only the fixed narrow cone and the labels whose frozen selector is nonzero. Thus the wide error-cone carrier bound never enters the constants, and inactive synthesis profiles need no annular hypothesis.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenSlot_fourier_eq line 18
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_main_square_active_tail line 30
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_centered_masked_variation_active_tail line 79
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_narrow_main_square_tail line 160
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_narrow_centered_masked_variation_tail line 218