OAI/Analysis/OperatorAlgebra/ScalarLpMultiplier.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Concrete bounded multipliers on scalar L². These are the actual spectral cutoffs used in the modular-core weight construction.

  1. lemma OAI.WeakPureInfiniteness.boundedScalarLp_mem line 16
  2. def OAI.WeakPureInfiniteness.boundedScalarLpApply line 24
  3. lemma OAI.WeakPureInfiniteness.boundedScalarLpApply_ae line 28
  4. def OAI.WeakPureInfiniteness.boundedScalarLpLinear line 33
  5. def OAI.WeakPureInfiniteness.boundedScalarLp line 54
  6. lemma OAI.WeakPureInfiniteness.boundedScalarLp_ae line 63
  7. lemma OAI.WeakPureInfiniteness.boundedScalarLp_norm_le line 68
  8. def OAI.WeakPureInfiniteness.scalarLpMultiplier line 73
  9. lemma OAI.WeakPureInfiniteness.scalarLpMultiplier_ae line 77
  10. lemma OAI.WeakPureInfiniteness.scalarLpMultiplier_mul line 80
  11. lemma OAI.WeakPureInfiniteness.scalarLpMultiplier_one line 93
  12. lemma OAI.WeakPureInfiniteness.scalarLpMultiplier_star line 101
  13. def OAI.WeakPureInfiniteness.scalarLpRepresentation line 115

    Source documentation

    Multiplication by bounded continuous scalar functions on actual L².

    def scalarLpRepresentation : BoundedContinuousFunction ℝ ℂ →⋆ₐ[ℂ]
    (Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) where
…
  14. lemma OAI.WeakPureInfiniteness.scalarLpRepresentation_character line 151