OAI/Analysis/LipschitzHilbert/Packets/PacketDataDensityJetNormalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The late mask normalization preserves the actual density forest, physical packet sums and masks. Its analytic constant has an explicit polynomial bound after the mask exponent has been chosen.

  1. def OAI.LipschitzHilbert.PacketLatticeData.PacketDensityForest.withJetControl line 17
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.withJetControl_physicalMaskedValue line 45
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.maskJetControl_referenceEnvelopeConstant line 57
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.mask_referenceEnvelopeConstant_of_ratio line 77
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.PacketDensityForest.mask_geometry line 86