lpMeasToLpTrimLie_symm_toLp — Mathlib

English

The symmetric version of lpMeasToLpTrimLie maps indicators to indicators in the trimmed space.

Русский

Симметричная версия lpMeasToLpTrimLie отображает индикаторы в индикаторы в обрезанном пространстве.

LaTeX

$$$(lpMeasToLpTrimLie\ F\ Real\ p μ hm).symm (indicatorConstLp p hs hμs c) = indicatorConstLp p (hm s hs) ((le_trim hm).trans_lt hμs.lt_top).ne c$$$

Lean4

theorem lpMeasToLpTrimLie_symm_toLp [one_le_p : Fact (1 ≤ p)] [NormedSpace ℝ F] (hm : m ≤ m0) (f : α → F)
    (hf : MemLp f p (μ.trim hm)) :
    ((lpMeasToLpTrimLie F ℝ p μ hm).symm (hf.toLp f) : Lp F p μ) = (memLp_of_memLp_trim hm hf).toLp f :=
  by
  ext1
  change lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf) =ᵐ[μ] (MemLp.toLp f _ : α → F)
  grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp hf), MemLp.coeFn_toLp]

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