OAI/Analysis/LipschitzHilbert/Trees/SourceTopWeightTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A top's reciprocal quadratic weight can be moved across a shorter tile by spending one fixed power of packet decay.

  1. theorem OAI.LipschitzHilbert.top_weight_base_transfer line 10
  2. theorem OAI.LipschitzHilbert.top_weight_envelope_transfer line 34