OAI/Analysis/LipschitzHilbert/Geometry/PacketDataDirectionLatticeCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The number of actual spatial lattice boxes through a point is bounded at one scale and label, uniformly in the comparison direction.

  1. theorem OAI.LipschitzHilbert.envelope_lower_near line 13

    Also declared: OAI/Analysis/LipschitzHilbert/Geometry/SourceDirectionLatticeCount.lean:13 (same declaration text).

  2. theorem OAI.LipschitzHilbert.PacketLatticeData.direction_lattice_count line 29