English
Let μ be a locally finite measure on ℝ. Then for every a,b ∈ ℝ, the function x ↦ (1+x^2)⁻¹ is μ-integrable on [a,b].
Русский
Пусть μ — локально конечная мера на ℝ. Тогда для любых a, b ∈ ℝ функция x ↦ (1+x^2)⁻¹ интегрируема по μ на отрезке [a,b].
LaTeX
$$$\forall a,b\in\mathbb{R},\ \int_{a}^{b} \frac{1}{1+x^{2}} \, d\mu < \infty$$$
Lean4
/-- If `f` is real-meromorphic on a compact interval, then `log ‖f ·‖` is interval integrable on this
interval.
-/
theorem intervalIntegrable_log_norm_meromorphicOn (hf : MeromorphicOn f [[a, b]]) :
IntervalIntegrable (log ‖f ·‖) volume a b :=
by
by_cases t₀ : ∀ u : [[a, b]], meromorphicOrderAt f u ≠ ⊤
· obtain ⟨g, h₁g, h₂g, h₃g⟩ :=
hf.extract_zeros_poles t₀ ((MeromorphicOn.divisor f [[a, b]]).finiteSupport isCompact_uIcc)
have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g
rw [intervalIntegrable_congr_codiscreteWithin (h₄g.filter_mono (Filter.codiscreteWithin.mono Set.uIoc_subset_uIcc))]
apply IntervalIntegrable.add
· apply IntervalIntegrable.finsum
intro i
apply IntervalIntegrable.const_mul
rw [(by ring : a = ((a - i) + i)), (by ring : b = ((b - i) + i))]
apply IntervalIntegrable.comp_sub_right (f := (log ‖·‖)) _ i
simp [norm_eq_abs, log_abs]
· apply ContinuousOn.intervalIntegrable
apply h₁g.continuousOn.norm.log
simp_all
· rw [← hf.exists_meromorphicOrderAt_ne_top_iff_forall (isConnected_Icc inf_le_sup)] at t₀
push_neg at t₀
have : (log ‖f ·‖) =ᶠ[Filter.codiscreteWithin (Ι a b)] 0 :=
by
apply Filter.EventuallyEq.filter_mono _ (Filter.codiscreteWithin.mono Set.uIoc_subset_uIcc)
filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin, Filter.self_mem_codiscreteWithin [[a, b]]] with x h₁x h₂x
simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]
left
by_contra hCon
simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]
rw [intervalIntegrable_congr_codiscreteWithin this]
apply Iff.mpr _root_.intervalIntegrable_const_iff
tauto
