PositiveConeIdeal.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The positive-cone criterion in KR02, Lemma 7.17(ii). The hypothesis records closure under actual coefficient conjugation. The conclusion is membership in the cone, not an absorption assumption.

def OAI.WeakPureInfiniteness.selfAdjointConjugation line 18
Source documentation
Conjugation on the real self-adjoint part.
```
def selfAdjointConjugation (d : A) : selfAdjoint A →L[ℝ] selfAdjoint A :=
…
```
lemma OAI.WeakPureInfiniteness.selfAdjointConjugation_apply line 35
def OAI.WeakPureInfiniteness.conjugateRealFunctional line 38
lemma OAI.WeakPureInfiniteness.conjugateRealFunctional_apply line 42

lemma OAI.WeakPureInfiniteness.sqrt_negPart_conjugation line 49

Source documentation

The negative part produces an explicit negative square by conjugation.

lemma sqrt_negPart_conjugation (a : selfAdjoint A) :
    star (CFC.sqrt (a : A)⁻) * (a : A) * CFC.sqrt (a : A)⁻ =
      -((a : A)⁻ * (a : A)⁻) := by
…

theorem OAI.WeakPureInfiniteness.mem_positive_cone_of_common_nullspace line 79

Source documentation

A closed positive cone stable under coefficient conjugation contains every positive functional whose square nullspace contains its common square nullspace. This is the precise functional-analytic step of KR02 Lemma 7.17(ii).

theorem mem_positive_cone_of_common_nullspace
    (K : Set (WeakDual ℝ (selfAdjoint A)))
    (hclosed : IsClosed K) (hconvex : Convex ℝ K) (hzero : 0 ∈ K)
    (hscale : ∀ t : ℝ, 0 ≤ t → ∀ φ ∈ K, t • φ ∈ K)
    (hpositive : ∀ φ ∈ K, ∀ a : selfAdjoint A, 0 ≤ (a : A) → 0 ≤ φ a)
    (hconjugate : ∀ φ ∈ K, ∀ d : A, conjugateRealFunctional φ d ∈ K)
    (φ₀ : WeakDual ℝ (selfAdjoint A))
    (hφ₀ : ∀ a : selfAdjoint A, 0 ≤ (a : A) → 0 ≤ φ₀ a)
    (hnull : ∀ x : A,
      (∀ φ ∈ K, φ ⟨star x * x, IsSelfAdjoint.star_mul_self x⟩ = 0) →
      φ₀ ⟨star x * x, IsSelfAdjoint.star_mul_self x⟩ = 0) : φ₀ ∈ K := by
…

Mentions: OAI.WeakPureInfiniteness.conjugateRealFunctional