OAI/Analysis/LipschitzHilbert/Trees/SourceLatticeConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual translated sheared lattice packets satisfy the simultaneous top and covariant-derivative concentration estimate. Only the published Lepingle input remains in the variation argument.

  1. theorem OAI.LipschitzHilbert.SourceLatticePacket.source_lattice_concentration line 15