OAI/Analysis/LipschitzHilbert/Trees/SourcePackedEnvelopeEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The short-envelope square bound from geometric packing. Centers may lie outside the top; the reciprocal top weight supplies localization.

  1. theorem OAI.LipschitzHilbert.tileEnvelope_two_le_one line 13
  2. theorem OAI.LipschitzHilbert.packed_envelope_energy line 21