English
The map u ↦ f • u is an isometry between L1 spaces with density μ.withDensity f and μ.
Русский
Отображение u ↦ f • u является изометрией между L1-пространствами с плотностью μ.withDensity f и μ.
LaTeX
$$withDensityLI μ (E := E) f_meas u$$
Lean4
/-- The map `u ↦ f • u` is an isometry between the `L^1` spaces for `μ.withDensity f` and `μ`. -/
noncomputable def withDensitySMulLI {f : α → ℝ≥0} (f_meas : Measurable f) :
Lp E 1 (μ.withDensity fun x => f x) →ₗᵢ[ℝ] Lp E 1 μ
where
toFun u := (memL1_smul_of_L1_withDensity f_meas u).toLp _
map_add' := by
intro u v
ext1
filter_upwards [(memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp,
(memL1_smul_of_L1_withDensity f_meas v).coeFn_toLp, (memL1_smul_of_L1_withDensity f_meas (u + v)).coeFn_toLp,
Lp.coeFn_add ((memL1_smul_of_L1_withDensity f_meas u).toLp _) ((memL1_smul_of_L1_withDensity f_meas v).toLp _),
(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 (Lp.coeFn_add u v)]
intro x hu hv huv h' h''
rw [huv, h', Pi.add_apply, hu, hv]
rcases eq_or_ne (f x) 0 with (hx | hx)
· simp only [hx, zero_smul, add_zero]
· rw [h'' _, Pi.add_apply, smul_add]
simpa only [Ne, ENNReal.coe_eq_zero] using hx
map_smul' := by
intro r u
ext1
filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 (Lp.coeFn_smul r u),
(memL1_smul_of_L1_withDensity f_meas (r • u)).coeFn_toLp,
Lp.coeFn_smul r ((memL1_smul_of_L1_withDensity f_meas u).toLp _),
(memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp]
intro x h h' h'' h'''
rw [RingHom.id_apply, h', h'', Pi.smul_apply, h''']
rcases eq_or_ne (f x) 0 with (hx | hx)
· simp only [hx, zero_smul, smul_zero]
· rw [h _, smul_comm, Pi.smul_apply]
simpa only [Ne, ENNReal.coe_eq_zero] using hx
norm_map' := by
intro u
simp only [eLpNorm, LinearMap.coe_mk, AddHom.coe_mk, one_ne_zero, ENNReal.one_ne_top, ENNReal.toReal_one, if_false,
eLpNorm', ENNReal.rpow_one, _root_.div_one, Lp.norm_def]
rw [lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas.coe_nnreal_ennreal
(Filter.Eventually.of_forall fun x => ENNReal.coe_lt_top)]
congr 1
apply lintegral_congr_ae
filter_upwards [(memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp] with x hx
rw [hx]
simp [NNReal.smul_def, enorm_smul]
