TwoRatioReindex.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Reindexing the extra family of lambda sites

Even and odd lambda sites absorb a second countable family. Mu sites are unchanged. This is the explicit state-preserving bijection used in the pointed infinite tensor-product absorption argument.

abbrev OAI.KadisonKastler.TwoRatioSite line 18
def OAI.KadisonKastler.twoRatioSiteParameter line 20
def OAI.KadisonKastler.lambdaAbsorptionSiteEquiv line 25
Source documentation
Interleave the original and extra lambda families, leaving mu sites in their original order.
```
def lambdaAbsorptionSiteEquiv : (TwoRatioSite ⊕ ℕ) ≃ TwoRatioSite :=
…
```
Mentions: OAI.KadisonKastler.TwoRatioSite
theorem OAI.KadisonKastler.lambdaAbsorptionSiteEquiv_old_lambda line 31
theorem OAI.KadisonKastler.lambdaAbsorptionSiteEquiv_new_lambda line 34
theorem OAI.KadisonKastler.lambdaAbsorptionSiteEquiv_mu line 37
theorem OAI.KadisonKastler.lambdaAbsorptionSiteEquiv_preserves_parameter line 41
Source documentation
Each site retains its density matrix parameter under the bijection.
```
theorem lambdaAbsorptionSiteEquiv_preserves_parameter (i : TwoRatioSite ⊕ ℕ) :
    twoRatioSiteParameter (lambdaAbsorptionSiteEquiv i) =
      Sum.elim twoRatioSiteParameter (fun _ => fixedProductLambda) i := by
…
```
Mentions: OAI.KadisonKastler.TwoRatioSite, OAI.KadisonKastler.twoRatioSiteParameter, OAI.KadisonKastler.lambdaAbsorptionSiteEquiv, OAI.KadisonKastler.fixedProductLambda
def OAI.KadisonKastler.twoSiteWeight line 47
Source documentation
The individual diagonal weights of the two-dimensional state.
```
def twoSiteWeight (ν : ℝ) (i : Fin 2) : ℝ :=
…
```
theorem OAI.KadisonKastler.lambdaAbsorptionSiteEquiv_preserves_weight line 50