OAI/Analysis/KadisonKastler/ModularLocalizedGraph.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A localized vector gives an approximate modular graph pair

The error depends only on the width of the logarithmic interval. No bound on its center is needed, and both graph coordinates approximate the same original vector after their separate positive scalar normalizations.

  1. theorem OAI.KadisonKastler.norm_scaled_error line 22
  2. theorem OAI.KadisonKastler.modular_localized_graph_pair line 35