English
If μ' is dominated by c' μ and μ ≤ c μ', and both T‑operators are dominated additive with the same T, then for any integrable f with respect to μ, the values of setToFun under μ and μ' coincide.
Русский
Если меры μ и μ' связаны как выше и функционалы T совпадают по обе стороны, то для интегрируемой f функции setToFun равны под μ и μ'.
LaTeX
$$$\\text{setToFun }(μ,T,hT,f)=\\text{setToFun }(μ',T,hT',f)$$$
Lean4
theorem setToFun_congr_measure_of_integrable {μ' : Measure α} (c' : ℝ≥0∞) (hc' : c' ≠ ∞) (hμ'_le : μ' ≤ c' • μ)
(hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ' T C') (f : α → E) (hfμ : Integrable f μ) :
setToFun μ T hT f = setToFun μ' T hT' f := by
-- integrability for `μ` implies integrability for `μ'`.
have h_int : ∀ g : α → E, Integrable g μ → Integrable g μ' := fun g hg => Integrable.of_measure_le_smul hc' hμ'_le hg
apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)
· intro c s hs hμs
have hμ's : μ' s ≠ ∞ := by
refine ((hμ'_le s).trans_lt ?_).ne
rw [Measure.smul_apply, smul_eq_mul]
exact ENNReal.mul_lt_top hc'.lt_top hμs
rw [setToFun_indicator_const hT hs hμs.ne, setToFun_indicator_const hT' hs hμ's]
· intro f₂ g₂ _ hf₂ hg₂ h_eq_f h_eq_g
rw [setToFun_add hT hf₂ hg₂, setToFun_add hT' (h_int f₂ hf₂) (h_int g₂ hg₂), h_eq_f, h_eq_g]
· refine isClosed_eq (continuous_setToFun hT) ?_
have :
(fun f : α →₁[μ] E => setToFun μ' T hT' f) = fun f : α →₁[μ] E =>
setToFun μ' T hT' ((h_int f (L1.integrable_coeFn f)).toL1 f) :=
by ext1 f; exact setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm
rw [this]
exact (continuous_setToFun hT').comp (continuous_L1_toL1 c' hc' hμ'_le)
· intro f₂ g₂ hfg _ hf_eq
have hfg' : f₂ =ᵐ[μ'] g₂ := (Measure.absolutelyContinuous_of_le_smul hμ'_le).ae_eq hfg
rw [← setToFun_congr_ae hT hfg, hf_eq, setToFun_congr_ae hT' hfg']
