eLpNorm_indicator_norm_ge_le — Mathlib

English

Let f be MemLp with p ∈ [0, ∞] and strongly measurable. For any ε > 0 there exists M such that the Lp-norm of the indicator tail of f over the tail set is bounded by ε: the Lp-norm of ( {x : M ≤ ∥f(x)∥_+}.indicator f ) is ≤ ε.

Русский

Пусть f ∈ MemLp(f, p, μ) и f сильно измерима. Для любого ε > 0 существует M, такое что Lp-норма tails'(f) ≤ ε.

LaTeX

$$$\exists M:\mathbb{R},\ eLpNorm({x| M \le \|f(x)\|_+}.indicator f)\, p\, μ \le \mathbb{ENNReal}(ε)$$$

Lean4

theorem eLpNorm_indicator_norm_ge_le (hf : MemLp f p μ) (hmeas : StronglyMeasurable f) {ε : ℝ} (hε : 0 < ε) :
    ∃ M : ℝ, eLpNorm ({x | M ≤ ‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε :=
  by
  by_cases hp_ne_zero : p = 0
  · refine ⟨1, hp_ne_zero.symm ▸ ?_⟩
    simp [eLpNorm_exponent_zero]
  by_cases hp_ne_top : p = ∞
  · subst hp_ne_top
    obtain ⟨M, hM⟩ := hf.eLpNormEssSup_indicator_norm_ge_eq_zero hmeas
    refine ⟨M, ?_⟩
    simp only [eLpNorm_exponent_top, hM, zero_le]
  obtain ⟨M, hM', hM⟩ :=
    MemLp.integral_indicator_norm_ge_nonneg_le (μ := μ) (hf.norm_rpow hp_ne_zero hp_ne_top)
      (Real.rpow_pos_of_pos hε p.toReal)
  refine ⟨M ^ (1 / p.toReal), ?_⟩
  rw [eLpNorm_eq_lintegral_rpow_enorm hp_ne_zero hp_ne_top, ← ENNReal.rpow_one (ENNReal.ofReal ε)]
  conv_rhs => rw [← mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm]
  rw [ENNReal.rpow_mul, ENNReal.rpow_le_rpow_iff (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top),
    ENNReal.ofReal_rpow_of_pos hε]
  convert hM using 3 with x
  rw [enorm_indicator_eq_indicator_enorm, enorm_indicator_eq_indicator_enorm]
  have hiff : M ^ (1 / p.toReal) ≤ ‖f x‖₊ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖₊ := by
    rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm, ←
      Real.rpow_le_rpow_iff hM' (Real.rpow_nonneg (norm_nonneg _) _)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top),
      ← Real.rpow_mul (norm_nonneg _), mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm,
      Real.rpow_one]
  by_cases hx : x ∈ {x : α | M ^ (1 / p.toReal) ≤ ‖f x‖₊}
  · rw [Set.indicator_of_mem hx, Set.indicator_of_mem, Real.enorm_of_nonneg (by positivity), ←
      ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) ENNReal.toReal_nonneg, ofReal_norm]
    rw [Set.mem_setOf_eq]
    rwa [← hiff]
  · rw [Set.indicator_of_notMem hx, Set.indicator_of_notMem]
    · simp [ENNReal.toReal_pos hp_ne_zero hp_ne_top]
    · rw [Set.mem_setOf_eq]
      rwa [← hiff]

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