OAI/Analysis/LipschitzHilbert/Estimates/JointLatticeAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete finite length/direction sum can use one product probability average of the actual translated lattices.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lattice_periodization_integrable line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.joint_lattice_average_bound line 44