English
There is a linear isometry between lpMeas F 𝕜 m p μ and Lp F p (μ.trim hm) given by lpMeasToLpTrimLie, with explicit inverse and linear structure.
Русский
Существует линейная изометрия между lpMeas и Lp через lpMeasToLpTrimLie; имеется явная обратная связь и линейная структура.
LaTeX
$$$lpMeasToLpTrimLie\ F\ 𝕜\ p\ μ hm : lpMeas F 𝕜 m p μ \to Lp F p (μ.trim hm)\; \text{isometry}$$$
Lean4
/-- `lpMeas` and `Lp F p (μ.trim hm)` are isometric, with a linear equivalence. -/
noncomputable def lpMeasToLpTrimLie [Fact (1 ≤ p)] (hm : m ≤ m0) : lpMeas F 𝕜 m p μ ≃ₗᵢ[𝕜] Lp F p (μ.trim hm)
where
toFun := lpMeasToLpTrim F 𝕜 p μ hm
invFun := lpTrimToLpMeas F 𝕜 p μ hm
left_inv := lpMeasSubgroupToLpTrim_left_inv hm
right_inv := lpMeasSubgroupToLpTrim_right_inv hm
map_add' := lpMeasSubgroupToLpTrim_add hm
map_smul' := lpMeasToLpTrim_smul hm
norm_map' := lpMeasSubgroupToLpTrim_norm_map hm
