OAI/Analysis/LipschitzHilbert/Trees/SourceMaskedTreeSplit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact short/frozen/error identity with an independent angular cutoff, and the corresponding integrated selector error.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.longOriginalLocal_mask_of_support line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.masked_ordinary_tree_split_identity line 45