partialTraj_const_restrict₂ — Mathlib

English

Let μ be a family of probability measures μn on Xn. If the kernels κn are constant, equal to μ(n+1), then the composition-product of these kernels over the finite interval {a+1, a+2, ..., b} collapses to the product measure over that interval. In other words, the restricted partial trajectory equals the product measure on Ioc(a,b).

Русский

Пусть μ — семейство распределений μn на пространствах Xn. Если ядра κn являются константными и равны μ(n+1), то композиция-ядро частичной траектории над промежутком {a+1, a+2, ..., b} совпадает с произведением этих распределений на этом интервале. Другими словами, ограниченное частичное траекторное ядро равно произведению меры на Ioc(a,b).

LaTeX

$$$$\left(\mathrm{partialTraj}\bigl(\lambda n \mapsto \mathrm{const}_{X_{n+1}}(\mu(n+1))\bigr)\;a\;b\right) \\mapsto \\left(\mathrm{restrict}_{2} Ioc\_subset\_Iic\_self\right) = \mathrm{const}\_\ast\bigl(\mathrm{Measure.pi}(\lambda i : Ioc(a,b) \mapsto \mu i)\bigr). $$$$

Lean4

/-- `partialTraj κ a b` is a kernel which up to an equivalence is equal to
`Kernel.id ×ₖ (κ a ⊗ₖ ... ⊗ₖ κ (b - 1))`. This lemma therefore states that if the kernels `κ`
are constant then their composition-product is the product measure. -/
theorem partialTraj_const_restrict₂ {a b : ℕ} :
    (partialTraj (fun n ↦ const _ (μ (n + 1))) a b).map (restrict₂ Ioc_subset_Iic_self) =
      const _ (Measure.pi (fun i : Ioc a b ↦ μ i)) :=
  by
  obtain hab | hba := lt_or_ge a b
  · refine Nat.le_induction ?_ (fun n hn hind ↦ ?_) b (Nat.succ_le.2 hab) <;> ext1 x₀
    · rw [partialTraj_succ_self, ← map_comp_right, map_apply, prod_apply, map_apply, const_apply, const_apply,
        Measure.map_piSingleton, restrict₂_comp_IicProdIoc, Measure.map_snd_prod, measure_univ, one_smul]
      all_goals fun_prop
    · have :
        (restrict₂ (Ioc_subset_Iic_self (a := a))) ∘ (IicProdIoc (X := X) n (n + 1)) =
          (IocProdIoc a n (n + 1)) ∘ (Prod.map (restrict₂ Ioc_subset_Iic_self) id) :=
        rfl
      rw [const_apply, partialTraj_succ_of_le (by cutsat), map_const, prod_const_comp, id_comp, ← map_comp_right, this,
        map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply, prod_apply, const_apply, const_apply,
        Measure.map_piSingleton, Measure.pi_prod_map_IocProdIoc]
      any_goals fun_prop
      all_goals cutsat
  · have : IsEmpty (Ioc a b) := by simpa [hba] using Subtype.isEmpty_false
    ext x s ms
    by_cases hs : s.Nonempty
    · rw [Subsingleton.eq_univ_of_nonempty hs, @measure_univ .., measure_univ]
      exact (IsMarkovKernel.map _ (measurable_restrict₂ _)) |>.isProbabilityMeasure x
    · rw [Set.not_nonempty_iff_eq_empty.1 hs]
      simp

Похожие утверждения