OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledRawEnvelope.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Carrier-free raw bounds for the original labeled lattices, before any bound on the total number of labels is imposed.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.absoluteConstant line 15
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.absoluteConstant_pos line 18
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.snappedSite line 24
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.snappedSite_injective line 28
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_swapped_joint_measurable line 32
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_absolute_envelope line 43
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_absolute_tileEnvelope line 66
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_eq_physical_slice line 91