OAI/Analysis/LipschitzHilbert/Trees/SourceEnvelopeWeightComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The quadratic reciprocal weight used for the packed short packets matches the long-tree product weight up to an absolute factor.

  1. theorem OAI.LipschitzHilbert.line_weight_product_lower line 11
  2. theorem OAI.LipschitzHilbert.envelope_tree_weight_lower line 28