OAI/Analysis/KadisonKastler/L2MeasurableExtension.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Extension by zero from a measurable L² stratum

  1. def OAI.KadisonKastler.l2ExtensionFunction line 17
  2. theorem OAI.KadisonKastler.l2ExtensionFunction_coe line 21
  3. theorem OAI.KadisonKastler.indicator_l2ExtensionFunction line 26
  4. theorem OAI.KadisonKastler.l2ExtensionMemLp line 34
  5. def OAI.KadisonKastler.l2Extend line 44
  6. theorem OAI.KadisonKastler.l2Extend_apply_ae line 47
  7. theorem OAI.KadisonKastler.l2Extend_norm line 51
  8. theorem OAI.KadisonKastler.ae_of_subtype_of_outside line 70
  9. theorem OAI.KadisonKastler.l2ExtensionFunction_add_ae line 80
  10. theorem OAI.KadisonKastler.l2ExtensionFunction_smul_ae line 93
  11. theorem OAI.KadisonKastler.l2Extend_add line 104
  12. theorem OAI.KadisonKastler.l2Extend_smul line 115
  13. def OAI.KadisonKastler.l2Extension line 126

    Source documentation

    Extension by zero is an isometric linear inclusion of each stratum.

    def l2Extension : Lp H 2 (Measure.comap ((↑) : s → X) μ) →ₗᵢ[ℂ] Lp H 2 μ where
…