OAI/Analysis/LipschitzHilbert/Trees/SourceComparablePlanarGram.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Comparable-scale Gram terms of actual planar vector packets are controlled by the sum of their single-scale energies.

  1. theorem OAI.LipschitzHilbert.comparable_planar_gram_energy line 13