English
If f is a simple function with values in G and g: G → F, then applying map to f and then setToSimpleFunc with T equals the finite sum, over the range of f, of T(f preimage of x) applied to g(x).
Русский
Если f — простая функция со значениями в G и g: G → F, то применение map к f затем setToSimpleFunc с T дает сумму по диапазону f: для каждого x берется T(f^{-1}({x})) применённое к g(x).
LaTeX
$$$ (f.map\, g).setToSimpleFunc T = \sum_{x \in f.range} T(f^{-1}(\{x\}))\,(g\,x) $$$
Lean4
theorem map_setToSimpleFunc (T : Set α → F →L[ℝ] F') (h_add : FinMeasAdditive μ T) {f : α →ₛ G} (hf : Integrable f μ)
{g : G → F} (hg : g 0 = 0) : (f.map g).setToSimpleFunc T = ∑ x ∈ f.range, T (f ⁻¹' { x }) (g x) := by
classical
have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero
have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' { x }) ≠ ∞ := fun x _ hx0 =>
(measure_preimage_lt_top_of_integrable f hf hx0).ne
simp only [setToSimpleFunc, range_map]
refine Finset.sum_image' _ fun b hb => ?_
rcases mem_range.1 hb with ⟨a, rfl⟩
by_cases h0 : g (f a) = 0
· simp_rw [h0]
rw [ContinuousLinearMap.map_zero, Finset.sum_eq_zero fun x hx => ?_]
rw [mem_filter] at hx
rw [hx.2, ContinuousLinearMap.map_zero]
have h_left_eq :
T (map g f ⁻¹' {g (f a)}) (g (f a)) = T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a)) := by
rw [map_preimage_singleton]
rw [h_left_eq]
have h_left_eq' :
T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a)) =
T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, f ⁻¹' { y }) (g (f a)) :=
by rw [← Finset.set_biUnion_preimage_singleton]
rw [h_left_eq']
rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
· simp only [sum_apply, ContinuousLinearMap.coe_sum']
refine Finset.sum_congr rfl fun x hx => ?_
rw [mem_filter] at hx
rw [hx.2]
· exact fun i => measurableSet_fiber _ _
· grind
· grind [Set.disjoint_iff]
