English
If f is in MemLp on q and is zero outside a set s of finite measure, then f is in MemLp with p ≤ q on μ as well.
Русский
Если f ∈ MemLp f q μ и поддержана внутри множества с конечной мерой, то f ∈ MemLp p μ для p ≤ q.
LaTeX
$$$MemLp f q μ \\Rightarrow (\\forall s, (hf: f|_{s^c}=0) \\land μ s ≠ ∞) \\Rightarrow MemLp f p μ$ при p ≤ q$$
Lean4
/-- If a function is supported on a finite-measure set and belongs to `ℒ^p`, then it belongs to
`ℒ^q` for any `q ≤ p`. -/
theorem mono_exponent_of_measure_support_ne_top {p q : ℝ≥0∞} {f : α → ε'} (hfq : MemLp f q μ) {s : Set α}
(hf : ∀ x, x ∉ s → f x = 0) (hs : μ s ≠ ∞) (hpq : p ≤ q) : MemLp f p μ :=
by
have : (toMeasurable μ s).indicator f = f :=
by
apply Set.indicator_eq_self.2
apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_
contrapose! hx
exact subset_toMeasurable μ s hx
rw [← this, memLp_indicator_iff_restrict (measurableSet_toMeasurable μ s)] at hfq ⊢
have : Fact (μ (toMeasurable μ s) < ∞) := ⟨by simpa [lt_top_iff_ne_top] using hs⟩
exact hfq.mono_exponent hpq
