exists_le_lowerSemicontinuous_lintegral_ge

English

The a.e. equality in the Lp Restrict CLM commutes with coeFn, i.e., the limit of the restricted map equals the restricted function value almost everywhere.

Русский

Эквивалентность a.e. для LpRestrictCLM совместима с вычислением coeFn: предел ограниченного отображения равен значению ограниченной функции почти повсюду.

LaTeX

$$$$LpToLpRestrictCLM\\_coeFn: a.e_{μ.restrict s}(f) = f|_s$$$$

Lean4

/-- Given a simple function `f` with values in `ℝ≥0`, there exists a lower 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_le_lowerSemicontinuous_lintegral_ge (f : α →ₛ ℝ≥0) {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
    ∃ g : α → ℝ≥0, (∀ x, f x ≤ g x) ∧ LowerSemicontinuous g ∧ (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, f x ∂μ) + ε := by
  induction f using MeasureTheory.SimpleFunc.induction generalizing ε with
  | @const c s hs =>
    let f := SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)
    by_cases h : ∫⁻ x, f x ∂μ = ⊤
    · refine ⟨fun _ => c, fun x => ?_, lowerSemicontinuous_const, by simp only [f, _root_.top_add, le_top, h]⟩
      simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero, Set.piecewise_eq_indicator,
        SimpleFunc.coe_piecewise]
      exact Set.indicator_le_self _ _ _
    by_cases hc : c = 0
    · refine ⟨fun _ => 0, ?_, lowerSemicontinuous_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]
      · simp only [lintegral_const, zero_mul, zero_le, ENNReal.coe_zero]
    have ne_top : μ s ≠ ⊤ := by
      classical
        simpa [f, hs, hc, lt_top_iff_ne_top, SimpleFunc.coe_const, Function.const_apply, lintegral_const,
        ENNReal.coe_indicator, Set.univ_inter, ENNReal.coe_ne_top, MeasurableSet.univ, ENNReal.mul_eq_top,
        SimpleFunc.const_zero, lintegral_indicator, ENNReal.coe_eq_zero, Ne, not_false_iff, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, restrict_apply] using h
    have : μ s < μ s + ε / c :=
      by
      have : (0 : ℝ≥0∞) < ε / c := ENNReal.div_pos_iff.2 ⟨ε0, ENNReal.coe_ne_top⟩
      simpa using ENNReal.add_lt_add_left ne_top this
    obtain ⟨u, su, u_open, μu⟩ : ∃ (u : _), u ⊇ s ∧ IsOpen u ∧ μ u < μ s + ε / c := s.exists_isOpen_lt_of_lt _ this
    refine ⟨Set.indicator u fun _ => c, fun x => ?_, u_open.lowerSemicontinuous_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 su (fun x => zero_le _) _
    · suffices (c : ℝ≥0∞) * μ u ≤ c * μ s + ε by
        classical
          simpa only [ENNReal.coe_indicator, u_open.measurableSet, lintegral_indicator, lintegral_const,
          MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, const_zero, coe_piecewise, coe_const, coe_zero,
          Set.piecewise_eq_indicator, Function.const_apply, hs]
      calc
        (c : ℝ≥0∞) * μ u ≤ c * (μ s + ε / c) := mul_le_mul_left' μu.le _
        _ = c * μ s + ε := by
          simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc
  | @add f₁ f₂ _ h₁ h₂ =>
    rcases h₁ (ENNReal.half_pos ε0).ne' with ⟨g₁, f₁_le_g₁, g₁cont, g₁int⟩
    rcases h₂ (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

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