English
The symmetrized lpMeasToLpTrimLie acts on indicators in a way that preserves indicator structure in the trimmed Lp space.
Русский
Симметризированное действие lpMeasToLpTrimLie на индикаторах сохраняет индикаторную структуру в обрезанном пространстве Lp.
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
/-- To prove something for an arbitrary `MemLp` 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 the `Lᵖ` space strongly measurable w.r.t. `m` for which the property
holds is closed.
* the property is closed under the almost-everywhere equal relation.
-/
@[elab_as_elim]
theorem induction_stronglyMeasurable (hm : m ≤ m0) (hp_ne_top : p ≠ ∞) (P : (α → F) → Prop)
(h_ind : ∀ (c : F) ⦃s⦄, MeasurableSet[m] s → μ s < ∞ → P (s.indicator fun _ => c))
(h_add :
∀ ⦃f g : α → F⦄,
Disjoint (Function.support f) (Function.support g) →
MemLp f p μ → MemLp g p μ → StronglyMeasurable[m] f → StronglyMeasurable[m] g → P f → P g → P (f + g))
(h_closed : IsClosed {f : lpMeas F ℝ m p μ | P f}) (h_ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g) :
∀ ⦃f : α → F⦄, MemLp f p μ → AEStronglyMeasurable[m] f μ → P f :=
by
intro f hf hfm
let f_Lp := hf.toLp f
have hfm_Lp : AEStronglyMeasurable[m] f_Lp μ := hfm.congr hf.coeFn_toLp.symm
refine h_ae hf.coeFn_toLp (Lp.memLp _) ?_
change P f_Lp
refine Lp.induction_stronglyMeasurable hm hp_ne_top (fun f => P f) ?_ ?_ h_closed f_Lp hfm_Lp
· intro c s hs hμs
rw [Lp.simpleFunc.coe_indicatorConst]
refine h_ae indicatorConstLp_coeFn.symm ?_ (h_ind c hs hμs)
exact memLp_indicator_const p (hm s hs) c (Or.inr hμs.ne)
· intro f g hf_mem hg_mem hfm hgm h_disj hfP hgP
have hfP' : P f := h_ae hf_mem.coeFn_toLp (Lp.memLp _) hfP
have hgP' : P g := h_ae hg_mem.coeFn_toLp (Lp.memLp _) hgP
specialize h_add h_disj hf_mem hg_mem hfm hgm hfP' hgP'
refine h_ae ?_ (hf_mem.add hg_mem) h_add
exact (hf_mem.coeFn_toLp.symm.add hg_mem.coeFn_toLp.symm).trans (Lp.coeFn_add _ _).symm
