OAI/Analysis/OInfinity/FockReturn.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The return map for the finite Fock approximation

The two coefficient families have complementary level weights. Their Gram maps have sum equal to the unit after normalization.

  1. def OAI.WeakPureInfiniteness.finiteFockAlgebraWord line 37
  2. def OAI.WeakPureInfiniteness.finiteFockUnweightedCoefficient line 40
  3. def OAI.WeakPureInfiniteness.finiteFockWeightedCoefficient line 43
  4. def OAI.WeakPureInfiniteness.finiteFockCuntzFamily line 47
  5. lemma OAI.WeakPureInfiniteness.finiteFockCuntzFamily_relations line 50
  6. lemma OAI.WeakPureInfiniteness.finiteFockWeightedCoefficient_square line 60
  7. lemma OAI.WeakPureInfiniteness.finiteFockCoefficient_normalization line 84
  8. def OAI.WeakPureInfiniteness.oInfinityFockReturn line 102
  9. lemma OAI.WeakPureInfiniteness.oInfinityFockReturn_one line 110
  10. lemma OAI.WeakPureInfiniteness.oInfinityFockReturn_cp line 118
  11. lemma OAI.WeakPureInfiniteness.oInfinityFockReturn_norm_le line 138