English
Let f(x) = O[l] g(x) uniformly on a measurable subset s of finite measure; then f is eventually integrable on s along l.
Русский
Пусть f(x)=O[l] g(x) равномерно на измеримой области s с конечной мерой; тогда f в конце концов интегрируема на s вдоль l.
LaTeX
$$$\\mathrm{eventually\\_integrableOn}\\bigl(f,g,l,s,\\mu\\bigr)$ with $f=O[𝓟s×ˢl](g\\circ Prod.snd)$$$
Lean4
/-- Let `f : X x Y → Z`. If as `y` tends to `l`, `f(x, y) = O(g(y))` uniformly on `s : Set X`
of finite measure, then f is eventually (as `y` tends to `l`) integrable along `s`. -/
theorem eventually_integrableOn [Norm F] (hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd))
(hfm : ∀ᶠ x in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)) (hs : MeasurableSet s) (hμ : μ s < ⊤) :
∀ᶠ x in l, IntegrableOn (fun i ↦ f (i, x)) s μ :=
by
obtain ⟨C, hC⟩ := hf.bound
obtain ⟨t, htl, ht⟩ := hC.exists_mem
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
obtain ⟨w, hwl, hw⟩ := hfm.exists_mem
refine eventually_iff_exists_mem.mpr ⟨w ∩ v, inter_mem hwl hv, fun x hx ↦ ?_⟩
haveI : IsFiniteMeasure (μ.restrict s) := ⟨Measure.restrict_apply_univ s ▸ hμ⟩
refine Integrable.mono' (integrable_const (C * ‖g x‖)) (hw x hx.1) ?_
filter_upwards [MeasureTheory.self_mem_ae_restrict hs]
intro y hy
exact ht (y, x) <| huv ⟨hu hy, hx.2⟩
