English
If two operator families T and T' agree on every measurable set s (with μ(s) finite), and μ admits FinMeasAdditive with respect to T, then for any integrable simple function f, setToSimpleFunc T f equals setToSimpleFunc T' f.
Русский
Если две семейства операторов T и T' совпадают на каждом измеримом множестве s (при конечной мере μ(s)), и μ обладает свойством FinMeasAdditive для T, то для любой интегрируемой простой функции f получаем equality setToSimpleFunc T f = setToSimpleFunc T' f.
LaTeX
$$$ (T, T') \text{ с тем же значением на всех } s: MeasurableSet s, \mu(s) < \infty) \Rightarrow setToSimpleFunc T f = setToSimpleFunc T' f $$$
Lean4
theorem setToSimpleFunc_congr' (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) {f g : α →ₛ E}
(hf : Integrable f μ) (hg : Integrable g μ) (h : Pairwise fun x y => T (f ⁻¹' { x } ∩ g ⁻¹' { y }) = 0) :
f.setToSimpleFunc T = g.setToSimpleFunc T :=
show ((pair f g).map Prod.fst).setToSimpleFunc T = ((pair f g).map Prod.snd).setToSimpleFunc T
by
have h_pair : Integrable (f.pair g) μ := integrable_pair hf hg
rw [map_setToSimpleFunc T h_add h_pair Prod.fst_zero]
rw [map_setToSimpleFunc T h_add h_pair Prod.snd_zero]
refine Finset.sum_congr rfl fun p hp => ?_
rcases mem_range.1 hp with ⟨a, rfl⟩
by_cases eq : f a = g a
· dsimp only [pair_apply]; rw [eq]
· have : T (pair f g ⁻¹' {(f a, g a)}) = 0 :=
by
have h_eq : T ((⇑(f.pair g)) ⁻¹' {(f a, g a)}) = T (f ⁻¹' {f a} ∩ g ⁻¹' {g a}) := by congr;
rw [pair_preimage_singleton f g]
rw [h_eq]
exact h eq
simp only [this, ContinuousLinearMap.zero_apply, pair_apply]
