OAI/Analysis/KadisonKastler/ProductIntegralUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rectangle tests determine an integrable product function

This finite-measure bridge will identify the range of the boundary projection. It uses uniqueness of vector measures on the rectangle pi-system, avoiding any unproved tensor-product identification of L2 spaces.

  1. theorem OAI.KadisonKastler.integrable_eq_zero_of_rectangle_integrals line 23
  2. theorem OAI.KadisonKastler.integrable_eq_of_rectangle_integrals line 40