OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledGoodQuantities.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Joint measurability of the actual reference quantities is needed before weighted bad-path sets are integrated over the physical plane.

  1. theorem OAI.LipschitzHilbert.lineEnvelope_continuous line 13
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainScale_joint_continuous line 24
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainSquare_joint_continuous line 36
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainSquareOnPlane line 44
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainSquareOnPlane_continuous line 48
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.measurableSet_error_or_main line 60