KMSBasisInvariant.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Inverse.KMSBasisInvariant.primalChange line 17
Source documentation
The invertible change of the ordered domain basis.
```
def primalChange (g : E ≃ₗ[F2] E) : (E →ₗ[F2] F) ≃ (E →ₗ[F2] F) where
…
```
def OAI.MaxCutGames.Inverse.KMSBasisInvariant.frequencyChange line 24
Source documentation
The contragredient reindexing used in the trace pairing.
```
def frequencyChange (g : E ≃ₗ[F2] E) : (F →ₗ[F2] E) ≃ (F →ₗ[F2] E) where
…
```
def OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant line 30
theorem OAI.MaxCutGames.Inverse.KMSBasisInvariant.character_change line 33
theorem OAI.MaxCutGames.Inverse.KMSBasisInvariant.coefficient_change line 42
Source documentation
Invariance of the function transfers to its actual normalized coefficients.
```
theorem coefficient_change (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) (g : E ≃ₗ[F2] E) (S : F →ₗ[F2] E) :
    linearCoeff f (g.toLinearMap.comp S) = linearCoeff f S := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant
def OAI.MaxCutGames.Inverse.KMSBasisInvariant.frequencyRank line 53
Source documentation
The degree is the rank of the actual dual linear map.
```
def frequencyRank (S : F →ₗ[F2] E) : ℕ := Module.finrank F2 (LinearMap.range S)
…
```
theorem OAI.MaxCutGames.Inverse.KMSBasisInvariant.frequencyRank_change line 56
def OAI.MaxCutGames.Inverse.KMSBasisInvariant.rankProjection line 64
Source documentation
Exact rank projection, defined directly by trace characters.
```
def rankProjection (i : ℕ) (f : (E →ₗ[F2] F) → ℝ) (X : E →ₗ[F2] F) : ℝ :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSBasisInvariant.rankProjection_invariant line 68
Source documentation
Each rank projection preserves basis invariance.
```
theorem rankProjection_invariant (i : ℕ) (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) : IsBasisInvariant (rankProjection i f) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSBasisInvariant.rankProjection