OAI/Analysis/OperatorAlgebra/ScalarVectorLp.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Elementary scalar/vector tensors in vector-valued L². These concrete maps supply the finite scalar blocks for expectation amplification.

  1. def OAI.WeakPureInfiniteness.scalarVectorLp line 17
  2. lemma OAI.WeakPureInfiniteness.scalarVectorLp_ae line 20
  3. lemma OAI.WeakPureInfiniteness.scalarVectorLp_norm line 24
  4. lemma OAI.WeakPureInfiniteness.scalarVectorLp_add_right line 35
  5. lemma OAI.WeakPureInfiniteness.scalarVectorLp_smul_right line 43
  6. def OAI.WeakPureInfiniteness.scalarVectorLpCLM line 50
  7. lemma OAI.WeakPureInfiniteness.scalarVectorLp_inner line 58
  8. lemma OAI.WeakPureInfiniteness.scalarVectorLp_pointwise line 71