PredualIdentification.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceNormalRieszOperator_mem line 13
Source documentation
The reconstructed operator belongs to the original algebra, by its verified double-commutant definition.
```
theorem sourceNormalRieszOperator_mem (θ : SourceCoordinate → ℝ)
    (F : StrongDual ℂ (SourceNormalPredualSpace θ)) :
    sourceNormalRieszOperator θ F ∈ sourceAlgebra θ := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceNormalPredualSpace, OAI.FiniteFactor.sourceNormalRieszOperator, OAI.FiniteFactor.sourceAlgebra
theorem OAI.FiniteFactor.sourceNormalFunctionals_ext line 43
Source documentation
Equality on actual vector functionals determines a functional on their closed span.
```
theorem sourceNormalFunctionals_ext (θ : SourceCoordinate → ℝ)
    (F G : StrongDual ℂ (SourceNormalPredualSpace θ))
    (h : ∀ ξ η, F (sourceVectorInSpace θ ξ η) = G (sourceVectorInSpace θ ξ η)) : F = G := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceNormalPredualSpace, OAI.FiniteFactor.sourceVectorInSpace
theorem OAI.FiniteFactor.sourceNormalEvaluation_surjective line 82
Source documentation
Every continuous functional on the constructed separable Banach space is evaluation by an element of the original source algebra.
```
theorem sourceNormalEvaluation_surjective (θ : SourceCoordinate → ℝ) :
    Function.Surjective (sourceNormalEvaluation θ) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceNormalEvaluation
theorem OAI.FiniteFactor.sourceNormalEvaluation_norm line 90
def OAI.FiniteFactor.sourceNormalEvaluationIsometry line 108
def OAI.FiniteFactor.sourcePredualIdentification line 117
Source documentation
The full dual identification, with the exact conjugate-linear convention required by Target.HasSeparablePredual.
```
def sourcePredualIdentification (θ : SourceCoordinate → ℝ) :
    StrongDual ℂ (SourceNormalPredualSpace θ) ≃ₗᵢ⋆[ℂ] SourceAlgebraSpace θ :=
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceNormalPredualSpace, OAI.FiniteFactor.SourceAlgebraSpace
theorem OAI.FiniteFactor.sourceAlgebra_hasSeparablePredual line 122