OAI/Analysis/OperatorAlgebra/ScalarSliceContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Norm-continuous scalar slices, used to regularize operators in the modular fixed-point algebra.

  1. lemma OAI.WeakPureInfiniteness.scalarVectorLpCLM_norm_le line 18
  2. def OAI.WeakPureInfiniteness.scalarVectorLpOperatorLinear line 23
  3. def OAI.WeakPureInfiniteness.scalarVectorLpOperator line 34
  4. lemma OAI.WeakPureInfiniteness.scalarOperatorSlice_continuous line 41
  5. lemma OAI.WeakPureInfiniteness.scalarOperatorSlice_norm_le line 52