English
A variant of measure-congruence: replacing μ by μ' with μ ≪ μ' leaves setToL1S unchanged on corresponding simple functions.
Русский
Замена μ на μ' с μ ≪ μ' не меняет setToL1S на соответствующих простых функциях.
LaTeX
$$$$\text{If } μ ≪ μ',\; setToL1S(T,f) = setToL1S(T,f') \text{ for } f,f'\text{ corresponding}.$$$$
Lean4
/-- `setToL1S` does not change if we replace the measure `μ` by `μ'` with `μ ≪ μ'`. The statement
uses two functions `f` and `f'` because they have to belong to different types, but morally these
are the same function (we have `f =ᵐ[μ] f'`). -/
theorem setToL1S_congr_measure {μ' : Measure α} (T : Set α → E →L[ℝ] F)
(h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hμ : μ ≪ μ') (f : α →₁ₛ[μ] E)
(f' : α →₁ₛ[μ'] E) (h : (f : α → E) =ᵐ[μ] f') : setToL1S T f = setToL1S T f' :=
by
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable f) ?_
refine (toSimpleFunc_eq_toFun f).trans ?_
suffices (f' : α → E) =ᵐ[μ] simpleFunc.toSimpleFunc f' from h.trans this
have goal' : (f' : α → E) =ᵐ[μ'] simpleFunc.toSimpleFunc f' := (toSimpleFunc_eq_toFun f').symm
exact hμ.ae_eq goal'
