OAI/Analysis/LipschitzHilbert/Packets/SourceDensityPacketGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Convert the actual density-forest radial assignment into the two coordinate bounds required by original-packet concentration.

  1. theorem OAI.LipschitzHilbert.SlopeBox.coordinates_of_radius_le line 11
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assigned_packet_geometry_of_density line 28