English
If μ and μ' are comparable in the sense of hT and hT_smul with integrable f, then the two setToFun values are equal.
Русский
Если f интегрируем по обеим мерам и слагаемые согласованы, то значения setToFun совпадают.
LaTeX
$$$\\mathrm{setToFun}\\;\\mu\\; T\\; hT\\; f = \\mathrm{setToFun}\\; (instHSMul.hSMul c \\mu)\\; T\\; hT_{\\text{smul}}\\; f$$$
Lean4
theorem setToFun_congr_smul_measure (c : ℝ≥0∞) (hc_ne_top : c ≠ ∞) (hT : DominatedFinMeasAdditive μ T C)
(hT_smul : DominatedFinMeasAdditive (c • μ) T C') (f : α → E) : setToFun μ T hT f = setToFun (c • μ) T hT_smul f :=
by
by_cases hc0 : c = 0
· simp [hc0] at hT_smul
have h : ∀ s, MeasurableSet s → μ s < ∞ → T s = 0 := fun s hs _ => hT_smul.eq_zero hs
rw [setToFun_zero_left' _ h, setToFun_measure_zero]
simp [hc0]
refine setToFun_congr_measure c⁻¹ c ?_ hc_ne_top (le_of_eq ?_) le_rfl hT hT_smul f
· simp [hc0]
· rw [smul_smul, ENNReal.inv_mul_cancel hc0 hc_ne_top, one_smul]
