OAI/Analysis/LipschitzHilbert/Packets/JointVectorPacketAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

All carrier components share the same site at each scale and direction. Averaging preserves the vector packet estimate without a dimension factor.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.joint_vector_convolution_packet_bound line 12