English
Applying lpMeasToLpTrimLie symmetrically to an indicator function yields the corresponding indicator in the larger Lp space.
Русский
Применение lpMeasToLpTrimLie к индикаторной функции даёт индикатор во множестве Lp большего сигма-алгебры.
LaTeX
$$$((lpMeasToLpTrimLie F \mathbb{R} 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
/-- When applying the inverse of `lpMeasToLpTrimLie` (which takes a function in the Lp space of
the sub-sigma algebra and returns its version in the larger Lp space) to an indicator of the
sub-sigma-algebra, we obtain an indicator in the Lp space of the larger sigma-algebra. -/
theorem lpMeasToLpTrimLie_symm_indicator [one_le_p : Fact (1 ≤ p)] [NormedSpace ℝ F] {hm : m ≤ m0} {s : Set α}
{μ : Measure α} (hs : MeasurableSet[m] s) (hμs : μ.trim hm s ≠ ∞) (c : F) :
((lpMeasToLpTrimLie F ℝ p μ hm).symm (indicatorConstLp p hs hμs c) : Lp F p μ) =
indicatorConstLp p (hm s hs) ((le_trim hm).trans_lt hμs.lt_top).ne c :=
by
ext1
change lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp p hs hμs c) =ᵐ[μ] (indicatorConstLp p _ _ c : α → F)
grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim indicatorConstLp_coeFn, indicatorConstLp_coeFn]
