OAI/Analysis/OperatorAlgebra/VectorLpMultiplier.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Scalar multiplication on vector-valued L², for the regular translation functional calculus in the modular core.

  1. lemma OAI.WeakPureInfiniteness.boundedVectorLp_mem line 17
  2. def OAI.WeakPureInfiniteness.boundedVectorLpApply line 25
  3. lemma OAI.WeakPureInfiniteness.boundedVectorLpApply_ae line 29
  4. def OAI.WeakPureInfiniteness.boundedVectorLpLinear line 34
  5. def OAI.WeakPureInfiniteness.boundedVectorLp line 53
  6. lemma OAI.WeakPureInfiniteness.boundedVectorLp_ae line 62
  7. def OAI.WeakPureInfiniteness.vectorLpMultiplier line 67
  8. lemma OAI.WeakPureInfiniteness.vectorLpMultiplier_ae line 70
  9. lemma OAI.WeakPureInfiniteness.vectorLpMultiplier_mul line 73
  10. lemma OAI.WeakPureInfiniteness.vectorLpMultiplier_one line 86
  11. lemma OAI.WeakPureInfiniteness.vectorLpMultiplier_star line 96
  12. def OAI.WeakPureInfiniteness.vectorLpRepresentation line 109

    Source documentation

    Bounded continuous scalar multipliers on vector-valued L².

    def vectorLpRepresentation : BoundedContinuousFunction ℝ ℂ →⋆ₐ[ℂ]
    (Lp H 2 μ →L[ℂ] Lp H 2 μ) where
…
  13. lemma OAI.WeakPureInfiniteness.vectorLpRepresentation_character line 145