English
The inverse map from lpMeasToLpTrimLie to MemLp yields the original function mapped into Lp, ensuring a canonical back-and-forth between representations.
Русский
Обратная карта lpMeasToLpTrimLie к MemLp возвращает исходную функцию, отображённую в Lp.
LaTeX
$$$(lpMeasToLpTrimLie\ F\ Real\ p μ hm).symm (hf.toLp f) = (memLp_of_memLp_trim hm hf).toLp f$$$
Lean4
/-- To prove something for an `Lp` function a.e. strongly measurable with respect to a
sub-σ-algebra `m` in a normed space, it suffices to show that
* the property holds for (multiples of) characteristic functions which are measurable w.r.t. `m`;
* is closed under addition;
* the set of functions in `Lp` strongly measurable w.r.t. `m` for which the property holds is
closed.
-/
@[elab_as_elim]
theorem induction_stronglyMeasurable (hm : m ≤ m0) (hp_ne_top : p ≠ ∞) (P : Lp F p μ → Prop)
(h_ind :
∀ (c : F) {s : Set α} (hs : MeasurableSet[m] s) (hμs : μ s < ∞),
P (Lp.simpleFunc.indicatorConst p (hm s hs) hμs.ne c))
(h_add :
∀ ⦃f g⦄,
∀ hf : MemLp f p μ,
∀ hg : MemLp g p μ,
StronglyMeasurable[m] f →
StronglyMeasurable[m] g →
Disjoint (Function.support f) (Function.support g) →
P (hf.toLp f) → P (hg.toLp g) → P (hf.toLp f + hg.toLp g))
(h_closed : IsClosed {f : lpMeas F ℝ m p μ | P f}) : ∀ f : Lp F p μ, AEStronglyMeasurable[m] f μ → P f :=
by
intro f hf
suffices h_add_ae :
∀ ⦃f g⦄,
∀ hf : MemLp f p μ,
∀ hg : MemLp g p μ,
AEStronglyMeasurable[m] f μ →
AEStronglyMeasurable[m] g μ →
Disjoint (Function.support f) (Function.support g) →
P (hf.toLp f) → P (hg.toLp g) → P (hf.toLp f + hg.toLp g)
from Lp.induction_stronglyMeasurable_aux hm hp_ne_top _ h_ind h_add_ae h_closed f hf
intro f g hf hg hfm hgm h_disj hPf hPg
let s_f : Set α := Function.support (hfm.mk f)
have hs_f : MeasurableSet[m] s_f := hfm.stronglyMeasurable_mk.measurableSet_support
have hs_f_eq : s_f =ᵐ[μ] Function.support f := hfm.ae_eq_mk.symm.support
let s_g : Set α := Function.support (hgm.mk g)
have hs_g : MeasurableSet[m] s_g := hgm.stronglyMeasurable_mk.measurableSet_support
have hs_g_eq : s_g =ᵐ[μ] Function.support g := hgm.ae_eq_mk.symm.support
have h_inter_empty : (s_f ∩ s_g : Set α) =ᵐ[μ] (∅ : Set α) :=
by
refine (hs_f_eq.inter hs_g_eq).trans ?_
suffices Function.support f ∩ Function.support g = ∅ by rw [this]
exact Set.disjoint_iff_inter_eq_empty.mp h_disj
let f' := (s_f \ s_g).indicator (hfm.mk f)
have hff' : f =ᵐ[μ] f' :=
by
have : s_f \ s_g =ᵐ[μ] s_f := by
rw [← Set.diff_inter_self_eq_diff, Set.inter_comm]
refine ((ae_eq_refl s_f).diff h_inter_empty).trans ?_
rw [Set.diff_empty]
refine ((indicator_ae_eq_of_ae_eq_set this).trans ?_).symm
rw [Set.indicator_support]
exact hfm.ae_eq_mk.symm
have hf'_meas : StronglyMeasurable[m] f' := hfm.stronglyMeasurable_mk.indicator (hs_f.diff hs_g)
have hf'_Lp : MemLp f' p μ := hf.ae_eq hff'
let g' := (s_g \ s_f).indicator (hgm.mk g)
have hgg' : g =ᵐ[μ] g' :=
by
have : s_g \ s_f =ᵐ[μ] s_g := by
rw [← Set.diff_inter_self_eq_diff]
refine ((ae_eq_refl s_g).diff h_inter_empty).trans ?_
rw [Set.diff_empty]
refine ((indicator_ae_eq_of_ae_eq_set this).trans ?_).symm
rw [Set.indicator_support]
exact hgm.ae_eq_mk.symm
have hg'_meas : StronglyMeasurable[m] g' := hgm.stronglyMeasurable_mk.indicator (hs_g.diff hs_f)
have hg'_Lp : MemLp g' p μ := hg.ae_eq hgg'
have h_disj : Disjoint (Function.support f') (Function.support g') :=
haveI : Disjoint (s_f \ s_g) (s_g \ s_f) := disjoint_sdiff_sdiff
this.mono Set.support_indicator_subset Set.support_indicator_subset
rw [← MemLp.toLp_congr hf'_Lp hf hff'.symm] at hPf ⊢
rw [← MemLp.toLp_congr hg'_Lp hg hgg'.symm] at hPg ⊢
exact h_add hf'_Lp hg'_Lp hf'_meas hg'_meas h_disj hPf hPg
