PredualRange.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

An actual separable Banach predual for the constructed matrix-generated factor. The existential convention is exactly Generator.HasSeparablePredual.

theorem OAI.Generator.Tracial.cyclicPredualEvaluation_surjective line 20
def OAI.Generator.Tracial.cyclicPredualLinearEquiv line 35
def OAI.Generator.Tracial.algebraStarIsometry line 39
def OAI.Generator.Tracial.cyclicPredualDualEquiv line 46
theorem OAI.Generator.Tracial.hasSeparablePredual_of_trace_separable line 49
theorem OAI.Generator.FiniteMatrixStage.generated_hasSeparablePredual line 64
theorem OAI.Generator.FiniteMatrixStage.exists_irreducible_matrix_generated_II1_separablePredual line 70
theorem OAI.Generator.Tracial.cyclicCoefficient_traceVector_injective line 104
Source documentation
A vector is determined by its trace-vector coefficient functional.
```
theorem cyclicCoefficient_traceVector_injective :
    Function.Injective (fun ξ : traceCyclicSpace τ =>
      cyclicCoefficient τ ξ (traceCyclicVector τ)) := by
…
```
Mentions: OAI.Generator.Tracial.traceCyclicSpace, OAI.Generator.Tracial.cyclicCoefficient, OAI.Generator.Tracial.traceCyclicVector
theorem OAI.Generator.Tracial.exists_countable_total_traceVectors line 114
Source documentation
A countable total family of dual evaluations supplies a countable total family of actual trace vectors.
```
theorem exists_countable_total_traceVectors
    [TopologicalSpace.SeparableSpace (cyclicPredual τ)] :
    ∃ a : ℕ → M.toStarSubalgebra, (∀ n, ‖a n‖ ≤ 1) ∧
      ∀ ξ : traceCyclicSpace τ,
        (∀ n, inner ℂ ξ (traceCyclicHom τ (a n) (traceCyclicVector τ)) = 0) → ξ = 0 := by
…
```
Mentions: OAI.Generator.Tracial.cyclicPredual, OAI.Generator.Tracial.traceCyclicSpace, OAI.Generator.Tracial.traceCyclicHom, OAI.Generator.Tracial.traceCyclicVector
theorem OAI.Generator.Tracial.traceCyclicSpace_separable_of_cyclicPredual line 134
theorem OAI.Generator.Tracial.traceOrbit_isSeparable_of_cyclicPredual line 154
instance OAI.Generator.predualAlgebraDualNormed line 174
Source documentation
Keep the norm topology explicit through the nested dual construction.
```
instance predualAlgebraDualNormed : NormedAddCommGroup (StrongDual ℂ S) := inferInstance
```
def OAI.Generator.predualFunctionals line 176
instance OAI.Generator.predualFunctionals_normed line 179
instance OAI.Generator.predualFunctionals_normedSpace line 181
def OAI.Generator.predualFunctionalsEquiv line 183
theorem OAI.Generator.predualFunctionalsEquiv_val line 186
theorem OAI.Generator.predualFunctionals_isClosed line 189
theorem OAI.Generator.predualFunctionals_separable line 193
def OAI.Generator.predualRangeEvaluation line 197
theorem OAI.Generator.predualRangeEvaluation_apply line 200
theorem OAI.Generator.predualRangeEvaluation_norm line 203
def OAI.Generator.predualRangePullback line 216
Source documentation
Pull a dual functional back through the conjugate-linear range equivalence.
```
def predualRangePullback (φ : StrongDual ℂ (predualFunctionals S e)) : StrongDual ℂ X :=
…
```
Mentions: OAI.Generator.predualFunctionals
theorem OAI.Generator.predualRangeEvaluation_surjective line 231
Source documentation
Every functional on the embedded given predual is evaluation at an actual a in S.
```
theorem predualRangeEvaluation_surjective : Function.Surjective (predualRangeEvaluation S e) := by
…
```
Mentions: OAI.Generator.predualRangeEvaluation
theorem OAI.Generator.predualFunctionals_eq_of_le line 252
Source documentation
A closed separating predual contained in an evaluation predual equals it. The inclusion is a substantive hypothesis, not supplied by this theorem.
```
theorem predualFunctionals_eq_of_le (F : Submodule ℂ (StrongDual ℂ S))
    (hincl : predualFunctionals S e ≤ F)
    (hdual : ∀ φ : StrongDual ℂ F, ∃ a : S, ∀ f : F, φ f = f.val a) :
    predualFunctionals S e = F := by
…
```
Mentions: OAI.Generator.predualFunctionals
theorem OAI.Generator.Tracial.predualFunctionals_eq_cyclicPredual_of_membership line 298
Source documentation
Normal-functional membership is sufficient for equality with the given predual.
```
theorem predualFunctionals_eq_cyclicPredual_of_membership
    (hmem : ∀ x : X, predualFunctional M.toStarSubalgebra e x ∈ cyclicPredual τ) :
    predualFunctionals M.toStarSubalgebra e = cyclicPredual τ := by
…
```
Mentions: OAI.Generator.predualFunctional, OAI.Generator.Tracial.cyclicPredual, OAI.Generator.predualFunctionals
theorem OAI.Generator.Tracial.cyclicPredual_separable_of_given_membership line 310
Source documentation
Under the same explicit membership input, separability transfers to the cyclic predual.
```
theorem cyclicPredual_separable_of_given_membership [TopologicalSpace.SeparableSpace X]
    (hmem : ∀ x : X, predualFunctional M.toStarSubalgebra e x ∈ cyclicPredual τ) :
    TopologicalSpace.SeparableSpace (cyclicPredual τ) := by
…
```
Mentions: OAI.Generator.predualFunctional, OAI.Generator.Tracial.cyclicPredual
theorem OAI.Generator.Tracial.given_predual_membership_iff_unitBall_continuity line 321
theorem OAI.Generator.Tracial.traceOrbit_isSeparable_of_given_membership line 327
theorem OAI.Generator.Tracial.traceOrbit_isSeparable_of_given_unitBall_continuity line 333