English
There is an isometry between lpMeasSubgroup F m p μ and Lp F p (μ.trim hm) providing a canonical isometric equivalence.
Русский
Существует изометрическое соответствие между lpMeasSubgroup и LpF p(μ.trim hm).
LaTeX
$$$lpMeasSubgroupToLpTrimIso\ F\ p\ μ hm : lpMeasSubgroup F m p μ \cong_i Lp F p (μ.trim hm)$$$
Lean4
/-- Auxiliary lemma for `Lp.induction_stronglyMeasurable`. -/
@[elab_as_elim]
theorem induction_stronglyMeasurable_aux (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 μ,
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))
(h_closed : IsClosed {f : lpMeas F ℝ m p μ | P f}) : ∀ f : Lp F p μ, AEStronglyMeasurable[m] f μ → P f :=
by
intro f hf
let f' := (⟨f, hf⟩ : lpMeas F ℝ m p μ)
let g := lpMeasToLpTrimLie F ℝ p μ hm f'
have hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g := by simp only [f', g, LinearIsometryEquiv.symm_apply_apply]
change P ↑f'
rw [hfg]
refine @Lp.induction α F m _ p (μ.trim hm) _ hp_ne_top (fun g => P ((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) ?_ ?_ ?_ g
· intro b t ht hμt
rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator ht hμt.ne b]
have hμt' : μ t < ∞ := (le_trim hm).trans_lt hμt
specialize h_ind b ht hμt'
rwa [Lp.simpleFunc.coe_indicatorConst] at h_ind
· intro f g hf hg h_disj hfP hgP
rw [LinearIsometryEquiv.map_add]
push_cast
have h_eq :
∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf) : Lp F p μ) = (memLp_of_memLp_trim hm hf).toLp f :=
lpMeasToLpTrimLie_symm_toLp hm
rw [h_eq f hf] at hfP ⊢
rw [h_eq g hg] at hgP ⊢
exact
h_add (memLp_of_memLp_trim hm hf) (memLp_of_memLp_trim hm hg) (hf.aestronglyMeasurable.of_trim hm)
(hg.aestronglyMeasurable.of_trim hm) h_disj hfP hgP
· change IsClosed ((lpMeasToLpTrimLie F ℝ p μ hm).symm ⁻¹' {g : lpMeas F ℝ m p μ | P ↑g})
exact IsClosed.preimage (LinearIsometryEquiv.continuous _) h_closed
