English
If μ' is dominated by a scalar multiple c' of μ with c' finite, the L1‑lifting operation sending a μ‑integrable function to its L1 representation is continuous in f, even when the underlying measure is changed to μ'.
Русский
Пусть μ' ограничена отношением μ' ≤ c' μ и c' конечен. Тогда отображение, отправляющее f в L1‑представление по мере μ, непрерывно по отношению к f при переходе к μ'.
LaTeX
$$$\\text{continuous } f \\mapsto ((\\mathrm{Integrable.of\\_measure\\_le\\_smul}\\; hc'\\; hμ'\\le μ) (L1.integrable\\_coeFn\\; f)).toL1 f$$$
Lean4
/-- Auxiliary lemma for `setToFun_congr_measure`: the function sending `f : α →₁[μ] G` to
`f : α →₁[μ'] G` is continuous when `μ' ≤ c' • μ` for `c' ≠ ∞`. -/
theorem continuous_L1_toL1 {μ' : Measure α} (c' : ℝ≥0∞) (hc' : c' ≠ ∞) (hμ'_le : μ' ≤ c' • μ) :
Continuous fun f : α →₁[μ] G => (Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f)).toL1 f :=
by
by_cases hc'0 : c' = 0
· have hμ'0 : μ' = 0 := by rw [← Measure.nonpos_iff_eq_zero']; refine hμ'_le.trans ?_; simp [hc'0]
have h_im_zero :
(fun f : α →₁[μ] G => (Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f)).toL1 f) = 0 := by ext1 f;
ext1; simp_rw [hμ'0]; simp only [ae_zero, EventuallyEq, eventually_bot]
rw [h_im_zero]
exact continuous_zero
rw [Metric.continuous_iff]
intro f ε hε_pos
use ε / 2 / c'.toReal
refine ⟨div_pos (half_pos hε_pos) (toReal_pos hc'0 hc'), ?_⟩
intro g hfg
rw [Lp.dist_def] at hfg ⊢
let h_int := fun f' : α →₁[μ] G => (L1.integrable_coeFn f').of_measure_le_smul hc' hμ'_le
have : eLpNorm (⇑(Integrable.toL1 g (h_int g)) - ⇑(Integrable.toL1 f (h_int f))) 1 μ' = eLpNorm (⇑g - ⇑f) 1 μ' :=
eLpNorm_congr_ae ((Integrable.coeFn_toL1 _).sub (Integrable.coeFn_toL1 _))
rw [this]
have h_eLpNorm_ne_top : eLpNorm (⇑g - ⇑f) 1 μ ≠ ∞ := by rw [← eLpNorm_congr_ae (Lp.coeFn_sub _ _)];
exact Lp.eLpNorm_ne_top _
calc
(eLpNorm (⇑g - ⇑f) 1 μ').toReal ≤ (c' * eLpNorm (⇑g - ⇑f) 1 μ).toReal :=
by
refine toReal_mono (ENNReal.mul_ne_top hc' h_eLpNorm_ne_top) ?_
refine (eLpNorm_mono_measure (⇑g - ⇑f) hμ'_le).trans_eq ?_
rw [eLpNorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]
simp
_ = c'.toReal * (eLpNorm (⇑g - ⇑f) 1 μ).toReal := toReal_mul
_ ≤ c'.toReal * (ε / 2 / c'.toReal) := by gcongr
_ = ε / 2 := by refine mul_div_cancel₀ (ε / 2) ?_; rw [Ne, toReal_eq_zero_iff]; simp [hc', hc'0]
_ < ε := half_lt_self hε_pos
