OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledMainTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Physical main-square and masked-variation tails after exact recombination of the fixed narrow-label slots. Constants are selected before the packet family, its scale range, and the physical interval.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainSquare line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainSquare_continuous line 21
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_main_square_tail line 41
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_centered_masked_variation_tail line 86