OAI/Analysis/LipschitzHilbert/Trees/SourceSelectedReferenceData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A selected reference family retains the original physical packets, coefficients and top masks. Its spatial item type depends on the selected finite subset, while its good event directly controls the original selected stopping prefixes and all unary runs.

  1. def OAI.LipschitzHilbert.PhysicalReferenceData.restrictPackets line 21
  2. theorem OAI.LipschitzHilbert.PhysicalReferenceData.restrictPackets_bad line 33
  3. theorem OAI.LipschitzHilbert.PhysicalReferenceData.selectedPrefix_good_bound line 41
  4. theorem OAI.LipschitzHilbert.PhysicalReferenceData.selectedPrefix_unary_good_bound line 50
  5. theorem OAI.LipschitzHilbert.eventually_selected_reference_prefix_area line 67