English
If μ' is added to μ and both T‑structures are DomFinAdditive, then setToFun for μ + μ' with hT_add equals setToFun for μ with hT.
Русский
Если к мере μ добавить μ' и обе структуры T удовлетворяют доминируемой конечной аддитивности, тогда setToFun(μ+μ', T_add, f) совпадает с setToFun(μ, T, f).
LaTeX
$$$\\mathrm{setToFun}(μ+μ',T\\, hT_{\\text{add}}\\, f)=\\mathrm{setToFun}(μ,T,hT,f)$$$
Lean4
theorem setToFun_congr_measure {μ' : Measure α} (c c' : ℝ≥0∞) (hc : c ≠ ∞) (hc' : c' ≠ ∞) (hμ_le : μ ≤ c • μ')
(hμ'_le : μ' ≤ c' • μ) (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ' T C') (f : α → E) :
setToFun μ T hT f = setToFun μ' T hT' f :=
by
by_cases hf : Integrable f μ
· exact setToFun_congr_measure_of_integrable c' hc' hμ'_le hT hT' f hf
· -- if `f` is not integrable, both `setToFun` are 0.
have h_int : ∀ g : α → E, ¬Integrable g μ → ¬Integrable g μ' := fun g => mt fun h => h.of_measure_le_smul hc hμ_le
simp_rw [setToFun_undef _ hf, setToFun_undef _ (h_int f hf)]
