OAI/Analysis/KadisonKastler/L2MeasurableRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Restricting L² vectors to a measurable stratum

The measure on a stratum is the comap of the restricted ambient measure. The restriction operator uses the original representative and is contractive.

  1. theorem OAI.KadisonKastler.l2RestrictMemLp line 25
  2. def OAI.KadisonKastler.l2Restrict line 30
  3. theorem OAI.KadisonKastler.l2Restrict_apply_ae line 33
  4. theorem OAI.KadisonKastler.l2Restrict_norm_le line 37
  5. theorem OAI.KadisonKastler.l2Restrict_add line 47
  6. theorem OAI.KadisonKastler.l2Restrict_smul line 61
  7. def OAI.KadisonKastler.l2Restriction line 73

    Source documentation

    The contractive linear restriction map to a measurable stratum.

    def l2Restriction : Lp H 2 μ →L[ℂ] Lp H 2 (Measure.comap ((↑) : s → X) μ) :=
…