PositiveSquareNullSpace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The closed linear left kernel used at the end of KR02 Lemma 7.18. The elementary-span hypothesis for the tensor ideal supplies the passage from elementary generators to its closure.

def OAI.WeakPureInfiniteness.positiveSquareNullSpace line 16
lemma OAI.WeakPureInfiniteness.positiveSquareNullSpace_closed line 28
lemma OAI.WeakPureInfiniteness.positiveFunctional_square_null_of_closure_span line 32

lemma OAI.WeakPureInfiniteness.common_nullspace_inclusion_of_elementary_span line 40

Source documentation

The last nullspace step of the published proof. The witness may depend on the elementary generator, as it does for the positive element x* x in KR02.

lemma common_nullspace_inclusion_of_elementary_span
    (K : Set (D →ₚ[ℂ] ℂ))
    (hconj : ∀ φ ∈ K, ∀ d : D, conjugatePositiveFunctional φ d ∈ K)
    (S : Set D)
    (hspan : ((commonSquareNullIdeal K hconj).module : Set D) ⊆
      closure (Submodule.span ℂ S : Set D))
    (hS : S ⊆ (commonSquareNullIdeal K hconj).module)
    (φ₀ : D →ₚ[ℂ] ℂ)
    (hfix : ∀ x ∈ S, ∃ φ ∈ K, φ₀ (star x * x) = φ (star x * x)) :
    ∀ x, commonSquareNull K x → φ₀ (star x * x) = 0 := by
…

Mentions: OAI.WeakPureInfiniteness.conjugatePositiveFunctional, OAI.WeakPureInfiniteness.commonSquareNullIdeal, OAI.WeakPureInfiniteness.commonSquareNull