English
If κ is a kernel and f_n are measurable, then withDensity κ (tsum_n f_n) = Kernel.sum (λ n, withDensity κ (f_n)).
Русский
Если κ — ядро, и каждое f_n измеримо, то withDensity κ (tsum_n f_n) равно сумме плотностей по κ: Kernel.sum (λ n, withDensity κ (f_n)).
LaTeX
$$$ \text{withDensity } κ (\sum' n, f_n) = \text{Kernel.sum } (\lambda n, \text{withDensity } κ (f_n)) $$$
Lean4
theorem withDensity_tsum [Countable ι] (κ : Kernel α β) [IsSFiniteKernel κ] {f : ι → α → β → ℝ≥0∞}
(hf : ∀ i, Measurable (Function.uncurry (f i))) :
withDensity κ (∑' n, f n) = Kernel.sum fun n => withDensity κ (f n) :=
by
have h_sum_a : ∀ a, Summable fun n => f n a := fun a => Pi.summable.mpr fun b => ENNReal.summable
have h_sum : Summable fun n => f n := Pi.summable.mpr h_sum_a
ext a s hs
rw [sum_apply' _ a hs, Kernel.withDensity_apply' κ _ a s]
swap
· have : Function.uncurry (∑' n, f n) = ∑' n, Function.uncurry (f n) :=
by
ext1 p
simp only [Function.uncurry_def]
rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]
exact Pi.summable.mpr fun p => ENNReal.summable
rw [this]
fun_prop
have : ∫⁻ b in s, (∑' n, f n) a b ∂κ a = ∫⁻ b in s, ∑' n, (fun b => f n a b) b ∂κ a :=
by
congr with b
rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]
rw [this, lintegral_tsum fun n => by fun_prop]
congr with n
rw [Kernel.withDensity_apply' _ (hf n) a s]
