OAI/Analysis/KadisonKastler/GraphScaleDirection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Directional graph bounds at all scales at least one

The integer row length is the ceiling of the squared scale. Both its moment cost and its graph metric remain uniformly controlled.

  1. theorem OAI.KadisonKastler.exists_bounded_graphRow_signal_scale line 20
  2. theorem OAI.KadisonKastler.graphProjectionDefect_le_of_row_scale line 75
  3. theorem OAI.KadisonKastler.norm_graphProjectionDefect_le_of_row_approx_scale line 134