OAI/Analysis/LipschitzHilbert/Estimates/NormalizedLatticeAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete finite scale/direction convolution sum follows from the bounds on its actual normalized finite packet models. Every carrier shares each spatial lattice, before taking the probability average.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.normalized_lattice_average_bound line 15