PositiveFunctionalKernel.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Positive-functional nullspace facts used in the proof of KR02 Lemma 7.17(ii). These work in the nonunital algebra and use its approximate unit.

def OAI.WeakPureInfiniteness.realFunctionalComplexification line 18
Source documentation
Complexification of a real functional on the self-adjoint part.
```
def realFunctionalComplexification (f : selfAdjoint A →ₗ[ℝ] ℝ) : A →ₗ[ℂ] ℂ where
…
```
lemma OAI.WeakPureInfiniteness.realFunctionalComplexification_apply line 27
def OAI.WeakPureInfiniteness.positiveRealComplexification line 37
Source documentation
Positivity alone suffices for the complexification; no unit or normalized state hypothesis is required.
```
def positiveRealComplexification (f : selfAdjoint A →ₗ[ℝ] ℝ)
    (hf : ∀ a : selfAdjoint A, 0 ≤ (a : A) → 0 ≤ f a) : A →ₚ[ℂ] ℂ where
…
```
lemma OAI.WeakPureInfiniteness.positiveRealComplexification_apply line 49
lemma OAI.WeakPureInfiniteness.positiveFunctional_eq_zero_of_square line 55
lemma OAI.WeakPureInfiniteness.positiveRealFunctional_eq_zero_of_square line 72