CoreSeparation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Constant operators from the original commutant commute with the full modular core. Their cyclic orbit separates core operators on the scalar subspace. This is the faithfulness step for the later weight construction; no trace or semifinite weight is assumed.

lemma OAI.WeakPureInfiniteness.pointwise_commutant_coefficient line 23
lemma OAI.WeakPureInfiniteness.pointwise_commutant_translate line 43
lemma OAI.WeakPureInfiniteness.pointwise_commutant_mem_core_commutant line 60
def OAI.WeakPureInfiniteness.indicatorVectorLinear line 89
Source documentation
A fixed finite-measure indicator as a continuous linear function of its vector coefficient.
```
def indicatorVectorLinear {s : Set ℝ} (hs : MeasurableSet s) (hμ : μ s ≠ ⊤) :
    H →ₗ[ℂ] Lp H 2 μ where
…
```
def OAI.WeakPureInfiniteness.indicatorVectorCLM line 104
lemma OAI.WeakPureInfiniteness.pointwise_indicatorVector line 113
lemma OAI.WeakPureInfiniteness.scalarInclusion_indicator line 126
theorem OAI.WeakPureInfiniteness.modularCore_eq_zero_of_scalarInclusion line 137
Source documentation
Vanishing on the scalar subspace detects an operator in the actual core.
```
theorem modularCore_eq_zero_of_scalarInclusion
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (hT : T ∈ modularCrossedProduct μ S)
    (hz : ∀ f : Lp ℂ 2 μ, T (modularScalarInclusion μ S f) = 0) : T = 0 := by
…
```
Mentions: OAI.WeakPureInfiniteness.modularCrossedProduct, OAI.WeakPureInfiniteness.modularScalarInclusion
theorem OAI.WeakPureInfiniteness.modularScalarCompression_faithful_square line 168
Source documentation
The scalar compression detects squares of elements of the core.
```
theorem modularScalarCompression_faithful_square
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (hT : T ∈ modularCrossedProduct μ S)
    (hz : modularScalarCompression μ S (star T * T) = 0) : T = 0 := by
…
```
Mentions: OAI.WeakPureInfiniteness.modularCrossedProduct, OAI.WeakPureInfiniteness.modularScalarCompression