English
If f is in L^p with 0<p<∞, then for every nonzero value y that f takes, the preimage f^{-1}({y}) has finite measure.
Русский
Для всякого ненулевого значения y, которое принимает f, множество f^{-1}({y}) имеет конечную меру.
LaTeX
$$$\\forall y\\ (y\\neq 0)\\; y\\in f(\\alpha)\\Rightarrow \\mu(f^{-1}(\\{y\\}))<\\infty$$$
Lean4
theorem measure_preimage_lt_top_of_memLp (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) (f : α →ₛ E) (hf : MemLp f p μ) (y : E)
(hy_ne : y ≠ 0) : μ (f ⁻¹' { y }) < ∞ :=
by
have hp_pos_real : 0 < p.toReal := ENNReal.toReal_pos hp_pos hp_ne_top
have hf_eLpNorm := MemLp.eLpNorm_lt_top hf
rw [eLpNorm_eq_eLpNorm' hp_pos hp_ne_top, f.eLpNorm'_eq, one_div, ←
@ENNReal.lt_rpow_inv_iff _ _ p.toReal⁻¹ (by simp [hp_pos_real]),
@ENNReal.top_rpow_of_pos p.toReal⁻¹⁻¹ (by simp [hp_pos_real]), ENNReal.sum_lt_top] at hf_eLpNorm
by_cases hyf : y ∈ f.range
swap
· suffices h_empty : f ⁻¹' { y } = ∅ by rw [h_empty, measure_empty]; exact ENNReal.coe_lt_top
ext1 x
rw [Set.mem_preimage, Set.mem_singleton_iff, mem_empty_iff_false, iff_false]
refine fun hxy => hyf ?_
rw [mem_range, Set.mem_range]
exact ⟨x, hxy⟩
specialize hf_eLpNorm y hyf
rw [ENNReal.mul_lt_top_iff] at hf_eLpNorm
cases hf_eLpNorm with
| inl hf_eLpNorm => exact hf_eLpNorm.2
| inr hf_eLpNorm =>
cases hf_eLpNorm with
| inl hf_eLpNorm =>
refine absurd ?_ hy_ne
simpa [hp_pos_real] using hf_eLpNorm
| inr hf_eLpNorm => simp [hf_eLpNorm]
