English
If κ ≤ κ', then for all n, a, x, s, the densityProcess with κ is not bigger than with κ'.
Русский
Если κ ≤ κ', то densityProcess(κ,·) не превосходит densityProcess(κ',·) для всех n, a, x, s.
LaTeX
$$$\forall n,a,x,s:\; \text{densityProcess}(\kappa,\nu,n,a,x,s) \le \text{densityProcess}(\kappa',\nu,n,a,x,s)$$$
Lean4
theorem setIntegral_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β}
(hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet[countableFiltration γ n] A) :
∫ x in A, densityProcess κ ν n a x s ∂(ν a) = (κ a).real (A ×ˢ s) :=
by
have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
obtain ⟨S, hS_subset, rfl⟩ := (measurableSet_generateFrom_countablePartition_iff _ _).mp hA
simp_rw [sUnion_eq_iUnion]
have h_disj : Pairwise (Disjoint on fun i : S ↦ (i : Set γ)) :=
by
intro u v huv
simp only [Function.onFun]
refine disjoint_countablePartition (hS_subset (by simp)) (hS_subset (by simp)) ?_
rwa [ne_eq, ← Subtype.ext_iff]
rw [integral_iUnion, iUnion_prod_const, measureReal_def, measure_iUnion,
ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
· congr with u
rw [setIntegral_densityProcess_of_mem hκν _ _ hs (hS_subset (by simp))]
rfl
· intro u v huv
simp only [Finset.coe_sort_coe, Set.disjoint_prod, disjoint_self, bot_eq_empty]
exact Or.inl (h_disj huv)
· exact fun _ ↦ (measurableSet_countablePartition n (hS_subset (by simp))).prod hs
· exact fun _ ↦ measurableSet_countablePartition n (hS_subset (by simp))
· exact h_disj
· exact (integrable_densityProcess hκν _ _ hs).integrableOn
