integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure

English

For a bounded continuous function, the integral under μ is bounded above by the liminf of integrals under μ_s, given appropriate open-set lower bounds.

Русский

Для ограниченной непрерывной функции интеграл по μ не превышает лиминф интегралов по μ_s при подходящих условиях снизу на открытых множествах.

LaTeX

$$$f: Ω\\to\\mathbb{R},\\; f\\ge 0,\\; (\\forall G\\text{ open})\\; μ(G) ≤ \\liminf_i μ_s(i,G) \\Rightarrow \\int f\,dμ ≤ \\liminf_i \\int f\,dμ_s(i)$$$

Lean4

theorem integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure {μ : Measure Ω} {μs : ℕ → Measure Ω}
    [∀ i, IsProbabilityMeasure (μs i)] {f : Ω →ᵇ ℝ} (f_nn : 0 ≤ f)
    (h_opens : ∀ G, IsOpen G → μ G ≤ atTop.liminf (fun i ↦ μs i G)) :
    ∫ x, (f x) ∂μ ≤ atTop.liminf (fun i ↦ ∫ x, (f x) ∂(μs i)) :=
  by
  have same := lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure f.continuous f_nn h_opens
  rw [@integral_eq_lintegral_of_nonneg_ae Ω _ μ f (Eventually.of_forall f_nn)
      f.continuous.measurable.aestronglyMeasurable]
  convert ENNReal.toReal_mono ?_ same
  · simp only [fun i ↦
        @integral_eq_lintegral_of_nonneg_ae Ω _ (μs i) f (Eventually.of_forall f_nn)
          f.continuous.measurable.aestronglyMeasurable]
    let g := BoundedContinuousFunction.comp _ Real.lipschitzWith_toNNReal f
    have bound : ∀ i, ∫⁻ x, ENNReal.ofReal (f x) ∂(μs i) ≤ nndist 0 g := fun i ↦ by
      simpa only [coe_nnreal_ennreal_nndist, measure_univ, mul_one, ge_iff_le] using
        BoundedContinuousFunction.lintegral_le_edist_mul (μ := μs i) g
    apply ENNReal.liminf_toReal_eq ENNReal.coe_ne_top (Eventually.of_forall bound)
  · apply ne_of_lt
    have obs := fun (i : ℕ) ↦ @BoundedContinuousFunction.lintegral_nnnorm_le Ω _ _ (μs i) ℝ _ f
    simp only [measure_univ, mul_one] at obs
    apply lt_of_le_of_lt _ (show (‖f‖₊ : ℝ≥0∞) < ∞ from ENNReal.coe_lt_top)
    apply liminf_le_of_le
    · refine ⟨0, .of_forall (by simp only [ge_iff_le, zero_le, forall_const])⟩
    · intro x hx
      obtain ⟨i, hi⟩ := hx.exists
      apply le_trans hi
      convert obs i with x
      have aux := ENNReal.ofReal_eq_coe_nnreal (f_nn x)
      simp only [ContinuousMap.toFun_eq_coe, BoundedContinuousFunction.coe_toContinuousMap] at aux
      rw [aux]
      congr
      exact (Real.norm_of_nonneg (f_nn x)).symm

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