English
If a function is Lipschitz on uIcc(a,b) with constant K, then it is absolutely continuous on [a,b].
Русский
Если функция липшицева на uIcc(a,b) с константой K, то она абсолютно непрерывна на [a,b].
LaTeX
$$$\text{LipschitzOnWith} K f (\mathrm{uIcc}(a,b)) \Rightarrow \text{AbsolutelyContinuousOnInterval}(f,a,b)$$$
Lean4
/-- `lpMeas F 𝕜 m p μ` is the subspace of `Lp F p μ` containing functions `f` verifying
`AEStronglyMeasurable[m] f μ`, i.e. functions which are `μ`-a.e. equal to
an `m`-strongly measurable function. -/
def lpMeas (m : MeasurableSpace α) [MeasurableSpace α] (p : ℝ≥0∞) (μ : Measure α) : Submodule 𝕜 (Lp F p μ)
where
carrier := {f : Lp F p μ | AEStronglyMeasurable[m] f μ}
zero_mem' := ⟨(0 : α → F), @stronglyMeasurable_zero _ _ m _ _, Lp.coeFn_zero _ _ _⟩
add_mem' {f g} hf hg := (hf.add hg).congr (Lp.coeFn_add f g).symm
smul_mem' c f hf := (hf.const_smul c).congr (Lp.coeFn_smul c f).symm
