exists_upperSemicontinuous_le_lintegral_le

English

For a simple function f taking nonnegative real values with finite integral, there exists an upper semicontinuous function g ≤ f such that the integral of f is not more than the integral of g plus ε.

Русский

Для простой функции f с неотрицательными значениями и конечным интегралом существует верхне-полусеполная функция g≤f такая, что интеграл f не превосходит интеграл g плюс ε.

LaTeX

$$$$\\exists g:\\; \\alpha \\to \\mathbb{R}_{\\ge 0},\\quad (g \\le f) \land UpperSemicontinuous(g) \land (\\int^{-} x, f(x) \\partial \\mu) \\le (\\int^{-} x, g(x) \\partial \\mu) + \\varepsilon.$$$$

Lean4

/-- Given a simple function `f` with values in `ℝ≥0`, there exists an upper semicontinuous
function `g ≤ f` with integral arbitrarily close to that of `f`. Formulation in terms of
`lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`. -/
theorem exists_upperSemicontinuous_le_lintegral_le (f : α →ₛ ℝ≥0) (int_f : (∫⁻ x, f x ∂μ) ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
    ∃ g : α → ℝ≥0, (∀ x, g x ≤ f x) ∧ UpperSemicontinuous g ∧ (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, g x ∂μ) + ε := by
  induction f using MeasureTheory.SimpleFunc.induction generalizing ε with
  | @const c s hs =>
    by_cases hc : c = 0
    · refine ⟨fun _ => 0, ?_, upperSemicontinuous_const, ?_⟩
      ·
        classical
          simp only [hc, Set.indicator_zero', Pi.zero_apply, SimpleFunc.const_zero, imp_true_iff, SimpleFunc.coe_zero,
          Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, le_zero_iff]
      ·
        classical
          simp only [hc, Set.indicator_zero', lintegral_const, zero_mul, Pi.zero_apply, SimpleFunc.const_zero, zero_add,
          zero_le', SimpleFunc.coe_zero, Set.piecewise_eq_indicator, ENNReal.coe_zero, SimpleFunc.coe_piecewise]
    have μs_lt_top : μ s < ∞ := by
      classical
        simpa only [hs, hc, lt_top_iff_ne_top, true_and, SimpleFunc.coe_const, or_false, lintegral_const,
        ENNReal.coe_indicator, Set.univ_inter, ENNReal.coe_ne_top, Measure.restrict_apply MeasurableSet.univ,
        ENNReal.mul_eq_top, SimpleFunc.const_zero, Function.const_apply, lintegral_indicator, ENNReal.coe_eq_zero, Ne,
        not_false_iff, SimpleFunc.coe_zero, Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, false_and] using int_f
    have : (0 : ℝ≥0∞) < ε / c := ENNReal.div_pos_iff.2 ⟨ε0, ENNReal.coe_ne_top⟩
    obtain ⟨F, Fs, F_closed, μF⟩ : ∃ (F : _), F ⊆ s ∧ IsClosed F ∧ μ s < μ F + ε / c :=
      hs.exists_isClosed_lt_add μs_lt_top.ne this.ne'
    refine ⟨Set.indicator F fun _ => c, fun x => ?_, F_closed.upperSemicontinuous_indicator (zero_le _), ?_⟩
    · simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero, Set.piecewise_eq_indicator,
        SimpleFunc.coe_piecewise]
      exact Set.indicator_le_indicator_of_subset Fs (fun x => zero_le _) _
    · suffices (c : ℝ≥0∞) * μ s ≤ c * μ F + ε by
        classical
          simpa only [hs, F_closed.measurableSet, SimpleFunc.coe_const, Function.const_apply, lintegral_const,
          ENNReal.coe_indicator, Set.univ_inter, MeasurableSet.univ, SimpleFunc.const_zero, lintegral_indicator,
          SimpleFunc.coe_zero, Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, Measure.restrict_apply]
      calc
        (c : ℝ≥0∞) * μ s ≤ c * (μ F + ε / c) := mul_le_mul_left' μF.le _
        _ = c * μ F + ε := by
          simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc
  | @add f₁ f₂ _ h₁
    h₂ =>
    have A : ((∫⁻ x : α, f₁ x ∂μ) + ∫⁻ x : α, f₂ x ∂μ) ≠ ⊤ := by
      rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]
    rcases h₁ (ENNReal.add_ne_top.1 A).1 (ENNReal.half_pos ε0).ne' with ⟨g₁, f₁_le_g₁, g₁cont, g₁int⟩
    rcases h₂ (ENNReal.add_ne_top.1 A).2 (ENNReal.half_pos ε0).ne' with ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩
    refine ⟨fun x => g₁ x + g₂ x, fun x => add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, ?_⟩
    simp only [SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply]
    rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal, lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal]
    convert add_le_add g₁int g₂int using 1
    conv_lhs => rw [← ENNReal.add_halves ε]
    abel

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