English
If s is measurable, then liftLinear applied to f and μ agrees with f applied to μ's outer measure on s: liftLinear f hf μ s = f μ.toOuterMeasure s for measurable s.
Русский
Если s измеримо, то liftLinear f hf μ по множеству s совпадает с f μ.toOuterMeasure на s: liftLinear f hf μ s = f μ.toOuterMeasure s.
LaTeX
$$$liftLinear f hf\\,\\mu\\,s = f\\mu^{\\text{toOuterMeasure}} (s)$$$
Lean4
/-- Lift a linear map between `OuterMeasure` spaces such that for each measure `μ` every measurable
set is caratheodory-measurable w.r.t. `f μ` to a linear map between `Measure` spaces. -/
noncomputable def liftLinear [MeasurableSpace β] (f : OuterMeasure α →ₗ[ℝ≥0∞] OuterMeasure β)
(hf : ∀ μ : Measure α, ‹_› ≤ (f μ.toOuterMeasure).caratheodory) : Measure α →ₗ[ℝ≥0∞] Measure β
where
toFun μ := (f μ.toOuterMeasure).toMeasure (hf μ)
map_add' μ₁
μ₂ :=
ext fun s hs => by
simp only [map_add, coe_add, Pi.add_apply, toMeasure_apply, add_toOuterMeasure, OuterMeasure.coe_add, hs]
map_smul' c
μ :=
ext fun s hs => by
simp only [LinearMap.map_smulₛₗ, Pi.smul_apply, toMeasure_apply, smul_toOuterMeasure (R := ℝ≥0∞),
OuterMeasure.coe_smul (R := ℝ≥0∞), smul_apply, hs]
