English
The densityProcess forms a martingale with respect to the countableFiltration, i.e., adapted and conditional expectation property holds.
Русский
DensityProcess образует мартингал относительно countableFiltration γ: адаптированность и условное ожидание выполняются.
LaTeX
$$$\text{Martingale}\big( (n, a) \mapsto \text{densityProcess}(\kappa,\nu,n,a,\cdot,\cdot), \text{countableFiltration }\gamma \big)$$$
Lean4
theorem setIntegral_densityProcess_of_mem (hκν : fst κ ≤ ν) [hν : IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β}
(hs : MeasurableSet s) {u : Set γ} (hu : u ∈ countablePartition γ n) :
∫ x in u, densityProcess κ ν n a x s ∂(ν a) = (κ a).real (u ×ˢ s) :=
by
have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
have hu_meas : MeasurableSet u := measurableSet_countablePartition n hu
simp_rw [densityProcess]
rw [integral_toReal]
rotate_left
· refine Measurable.aemeasurable ?_
change
Measurable
((fun (p : α × _) ↦ κ p.1 (countablePartitionSet n p.2 ×ˢ s) / ν p.1 (countablePartitionSet n p.2)) ∘
(fun x ↦ (a, x)))
exact (measurable_densityProcess_aux κ ν n hs).comp measurable_prodMk_left
· refine ae_of_all _ (fun x ↦ ?_)
by_cases h0 : ν a (countablePartitionSet n x) = 0
· suffices κ a (countablePartitionSet n x ×ˢ s) = 0 by simp [h0, this]
have h0' : fst κ a (countablePartitionSet n x) = 0 := le_antisymm ((hκν a _).trans h0.le) zero_le'
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h0'
refine measure_mono_null (fun x ↦ ?_) h0'
simp only [mem_prod, mem_setOf_eq, and_imp]
exact fun h _ ↦ h
· finiteness
congr
have :
∫⁻ x in u, κ a (countablePartitionSet n x ×ˢ s) / ν a (countablePartitionSet n x) ∂(ν a) =
∫⁻ _ in u, κ a (u ×ˢ s) / ν a u ∂(ν a) :=
by
refine setLIntegral_congr_fun hu_meas (fun t ht ↦ ?_)
rw [countablePartitionSet_of_mem hu ht]
rw [this]
simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
by_cases h0 : ν a u = 0
· simp only [h0, mul_zero]
have h0' : fst κ a u = 0 := le_antisymm ((hκν a _).trans h0.le) zero_le'
rw [fst_apply' _ _ hu_meas] at h0'
refine (measure_mono_null ?_ h0').symm
intro p
simp only [mem_prod, mem_setOf_eq, and_imp]
exact fun h _ ↦ h
rw [div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel h0, mul_one]
exact measure_ne_top _ _
