OAI/Analysis/KadisonKastler/TwoCornerStateNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Combining state comparisons on complementary corners

A functional centralizing a projection is the sum of its two compressed functionals. Comparing normalized corner states and their scalar weights therefore controls the norm distance of the original states.

  1. def OAI.KadisonKastler.cornerFunctional line 18
  2. theorem OAI.KadisonKastler.cornerFunctional_apply line 21
  3. theorem OAI.KadisonKastler.functional_eq_two_corners line 24
  4. theorem OAI.KadisonKastler.state_mixture_norm_sub_le line 37
  5. theorem OAI.KadisonKastler.twoCorner_state_norm_le line 62