OAI/Analysis/KadisonKastler/L2LinearFields.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Lifting fields of maps between different Hilbert spaces to L²

This supplies the varying synthesis maps used on a fixed dimension stratum. Measurability is required only after evaluation on a vector.

  1. theorem OAI.KadisonKastler.aestronglyMeasurable_linearField_apply line 24
  2. theorem OAI.KadisonKastler.l2LinearFieldMemLp line 45
  3. def OAI.KadisonKastler.l2LinearFieldApply line 54
  4. theorem OAI.KadisonKastler.l2LinearFieldApply_ae line 59
  5. def OAI.KadisonKastler.l2LinearFieldMap line 65
  6. theorem OAI.KadisonKastler.isometryField_norm_bound line 97
  7. def OAI.KadisonKastler.l2IsometryField line 102

    Source documentation

    Pointwise isometries give a genuine isometric inclusion of L² spaces.

    def l2IsometryField (U : X → E →ₗᵢ[ℂ] F)
    (hU : ∀ v, AEStronglyMeasurable (fun x => U x v) μ) :
    Lp E 2 μ →ₗᵢ[ℂ] Lp F 2 μ where
…
  8. theorem OAI.KadisonKastler.l2IsometryField_ae line 118