lintegral_Iic_eq_lintegral_Iio_add_Icc

English

There exists C>0 with ∫ exp(C‖x‖^2) finite (under μ) provided μ has rotation-invariant product and certain a>0 and bounds on μ({‖x‖≤a}).

Русский

Существет C>0 такое, что интеграл экспоненты от C‖x‖^2 по μ конечен, при условии вращательной инвариантности μ и подходящих a>0.

LaTeX

$$∃ C>0, Integrable( x ↦ exp(C‖x‖^2) ) μ$$

Lean4

/-- A Lebesgue Integral from -∞ to y can be expressed as the sum of one from -∞ to 0 and 0 to x -/
theorem lintegral_Iic_eq_lintegral_Iio_add_Icc {y z : ℝ} (f : ℝ → ℝ≥0∞) (hzy : z ≤ y) :
    ∫⁻ x in Iic y, f x = (∫⁻ x in Iio z, f x) + ∫⁻ x in Icc z y, f x :=
  by
  rw [← Iio_union_Icc_eq_Iic hzy, lintegral_union measurableSet_Icc]
  simp_rw [Set.disjoint_iff_forall_ne, mem_Iio, mem_Icc]
  intros
  linarith

Похожие утверждения