English
For a measurable set s with finite μ-measure, and x ∈ E, setToL1 hT applied to indicatorConstLp returns T s x.
Русский
Для измеримой области s с конечной мерой μ и вектора x ∈ E, применение SetToL1 к indicatorConstLp возвращает T s x.
LaTeX
$$$setToL1\, h_T\, (\text{indicatorConstLp}_{1}(s, μ|_s, x)) = T\, s\, x.$$$
Lean4
theorem setToL1_mono_left' {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, T s x ≤ T' s x)
(f : α →₁[μ] E) : setToL1 hT f ≤ setToL1 hT' f := by
induction f using Lp.induction (hp_ne_top := one_ne_top) with
| @indicatorConst c s hs
hμs =>
rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
exact hTT' s hs hμs c
| @add f g hf hg _ hf_le hg_le =>
rw [(setToL1 hT).map_add, (setToL1 hT').map_add]
exact add_le_add hf_le hg_le
| isClosed => exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous
