OAI/Analysis/LipschitzHilbert/Estimates/BoundedSupportedCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coordinate integrability follows from the vector indicator bound, without a factor depending on the number of coordinates.

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