Ionescu-Tulcea partialTraj restrictions

Stream: mathlib4

[Gaëtan Serré]

I'm trying to show that, if I have two families of Markov kernels that are equals on a pi set, then the restrictions of partialTraj to this set should be equals too. For now I have this:

import Mathlib

open MeasureTheory ProbabilityTheory Set

namespace MeasureTheory.Measure

variable {ι : Type*} [Fintype ι] {α : ι → Type*} [∀ i, MeasurableSpace (α i)]
  {μ ν : Measure (∀ i, α i)} [IsFiniteMeasure μ]

/-- Two measures on a finite product space are equal if they agree on all measurable rectangles
of the form `univ.pi s`, provided one of them is finite. -/
lemma pi_space_eq
    (h : ∀ s : ∀ i, Set (α i), (∀ i, MeasurableSet (s i)) → μ (univ.pi s) = ν (univ.pi s)) :
    μ = ν := by
  refine Measure.FiniteSpanningSetsIn.ext
    generateFrom_pi.symm (IsPiSystem.pi (fun _ => MeasurableSpace.isPiSystem_measurableSet)) ?_ ?_
  · refine { set := fun _ => univ, set_mem := ?_, finite := ?_, spanning := ?_ }
    · intro i
      use (fun _ => univ)
      refine ⟨?_, Set.pi_univ univ⟩
      exact mem_univ_pi.mpr (fun _ => MeasurableSet.univ)
    · exact fun _ => measure_lt_top _ _
    · exact iUnion_const univ
  · rintro _ ⟨s, hs, rfl⟩
    rw [mem_univ_pi] at hs
    exact h s hs

end MeasureTheory.Measure

variable {α : Type*} [MeasurableSpace α]
  (κ₁ κ₂ : (n : ℕ) → Kernel (Π _ : Finset.Iic n, α) α)
  [∀ n, IsMarkovKernel (κ₁ n)] [∀ n, IsMarkovKernel (κ₂ n)]
  {s : Set α} (hs : MeasurableSet s)
  (h : ∀ n, (univ.pi (fun _ => s)).EqOn (fun a => κ₁ n a) (fun a => κ₂ n a))

example {a b : ℕ} (hab : a ≤ b) : ∀ e ∈ univ.pi (fun _ => s),
    (Kernel.partialTraj (X := fun _ => α) κ₁ a b e).restrict (univ.pi (fun _ => s)) =
    (Kernel.partialTraj (X := fun _ => α) κ₂ a b e).restrict (univ.pi (fun _ => s)) := by
  intro e e_mem
  refine Measure.pi_space_eq ?_
  intro B B_m
  let C := fun i => (B i) ∩ s
  induction b, hab using Nat.le_induction with
    | base => simp
    | succ k h hk =>
      simp only [Kernel.partialTraj_succ_eq_comp h, Kernel.partialTraj_succ_self]
      sorry

(don't mind Measure.pi_space_eq, it probably already exists somewhere in Mathlib).

Like you can see, my first thought was to trying to prove it by induction but I'm getting stuck very quickly. I feel that it might be possible to prove this exact statement by continuing in this direction but I'm afraid it will become very difficult to unfold all these definitions.

I was wondering if there is a way to either change the statement or use another proof strategy (most likely both) to make the proof easier.

[Etienne Marion]

I am not at the computer right now but I can have a look later

[Gaëtan Serré]

Etienne Marion said:

I am not at the computer right now but I can have a look later

Sure, thanks a lot! Also thank you for work in formalizing this theorem

[Etienne Marion]

Ok, I managed to prove that the partialTraj associated to a family of restricted kernels is the restriction of the partialTraj, it should get you to your result easily. The only sorrys are measurability goals which shouldn't be an issue. I did not take the time to clean the proof up so it is quite messy, there are certainly many parts which can be factored out as separate lemmas to avoid all those measurability goals.

import Mathlib

open MeasureTheory ProbabilityTheory Finset Kernel

variable {X : ℕ → Type*} {mX : ∀ n, MeasurableSpace (X n)} {a b : ℕ} {κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))}

example {s : Π n, Set (X n)} [∀ n, IsSFiniteKernel (κ n)] (hs : ∀ n, MeasurableSet (s n)) (hab : a ≤ b) {x : Π i : Iic a, X i}
    (hx : x ∈ Set.univ.pi (fun i : Iic a ↦ s i)) :
    partialTraj (fun n ↦ (κ n).restrict (hs (n + 1))) a b x =
    (partialTraj κ a b x).restrict (Set.univ.pi (fun i ↦ s i)) := by
  induction b, hab using Nat.le_induction with
  | base =>
    simp only [partialTraj_self, id_apply]
    classical
    rw [restrict_dirac', if_pos hx]
    sorry
  | succ b hab hb =>
    ext t ht
    rw [partialTraj_succ_eq_comp hab, Kernel.comp_apply' _ _ _ ht, hb, Measure.restrict_apply ht,
      partialTraj_succ_eq_comp hab, Kernel.comp_apply',
      ← lintegral_add_compl (μ := partialTraj κ a b x) _ (.univ_pi fun i ↦ hs i),
      ← add_zero (∫⁻ _, _ ∂_)]
    · congrm ?_ + ?_
      · refine setLIntegral_congr_fun (.univ_pi fun i ↦ hs i) fun y hy ↦ ?_
        simp_rw [partialTraj_succ_self]
        rw [Kernel.map_apply', Kernel.id_prod_apply', Kernel.map_apply', Kernel.restrict_apply',
          Kernel.map_apply', Kernel.id_prod_apply', Kernel.map_apply']
        · congr
          ext z
          change _ ↔
            IicProdIoc b (b + 1) (y, MeasurableEquiv.piSingleton b z) ∈ Set.univ.pi (fun _ ↦ s _)
          simp [IicProdIoc, MeasurableEquiv.piSingleton]
          constructor
          · intro h i hi
            split_ifs with h'
            · simp only [Set.mem_pi, Set.mem_univ, forall_const, Subtype.forall, mem_Iic] at hy
              exact hy i h'
            obtain rfl : i = b + 1 := by omega
            exact h
          · intro h
            convert h (b + 1) le_rfl
            simp
        any_goals fun_prop
        all_goals sorry
      · symm
        apply setLIntegral_eq_zero
        · exact .compl (.univ_pi fun _ ↦ hs _)
        intro y hy
        simp only [Pi.zero_apply]
        rw [partialTraj_succ_self, Kernel.map_apply', Kernel.id_prod_apply', Kernel.map_apply']
        · convert measure_empty
          · ext z
            simp only [MeasurableEquiv.piSingleton, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk,
              Set.preimage_inter, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, Set.mem_univ,
              IicProdIoc, forall_const, Subtype.forall, mem_Iic, Set.mem_empty_iff_false, iff_false,
              not_and, not_forall]
            intro h1
            simp only [Set.mem_compl_iff, Set.mem_pi, Set.mem_univ, forall_const, Subtype.forall,
              mem_Iic, not_forall] at hy
            obtain ⟨i, hi1, hi2⟩ := hy
            refine ⟨i, by omega, ?_⟩
            simpa [hi1]
          infer_instance
        all_goals sorry
    · exact ht.inter (.univ_pi fun _ ↦ hs _)

[Etienne Marion]

I think the path you take was the right one, but it requires a bit of API about restriction to make the proof nice. Some of this API unfortunately requires some nasty unfolding, but I hope that we can identify a small set of lemmas which once proved will avoid unfolding in other proofs.

[Gaëtan Serré]

Wow thanks a lot! I did not expect you to prove this entirely :sweat_smile:! I'll prove the remaining sorries and, if I can, factor out some intermediate lemmas. I'm currently writing a paper about formalization of a theorem on meta global optimization algorithms and I wanted to use the Ionescu-Tulcea theorem to construct a measure on infinite sequence of iterations. I'll make sure to cite your paper as well as this discussion.

[Etienne Marion]

I'm glad I could help! It's really nice to see this part of the library being used :grinning_face_with_smiling_eyes:

[Gaëtan Serré]

Etienne Marion said:

I think the path you take was the right one, but it requires a bit of API about restriction to make the proof nice. Some of this API unfortunately requires some nasty unfolding, but I hope that we can identify a small set of lemmas which once proved will avoid unfolding in other proofs.

Ok that's reassuring. Indeed, I felt like it was very hard to "propagate" the restriction through the definition of partialTraj. Even getting access to the family of kernels that construct partialTraj was not trivial, but it might not be possible to make it easier.

[Gaëtan Serré]

I proved the sorries (I had to use a utility lemma to simplify the proofs on measurability. For some reasons, I did not found it in Mathlib) and I proved my original statement by induction.

import Mathlib

open MeasureTheory ProbabilityTheory Finset Kernel

namespace ProbabilityTheory

lemma measurableSet_apply {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {f : α → β}
    (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : MeasurableSet (f ⁻¹' s) := hf hs

variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] {a b : ℕ}
{κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1))}

/- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ionescu-Tulcea.20partialTraj.20restrictions -/

lemma Kernel.partialTraj_restrict {s : Π n, Set (X n)} [∀ n, IsSFiniteKernel (κ n)]
    (hs : ∀ n, MeasurableSet (s n)) (hab : a ≤ b) {x : Π i : Iic a, X i}
    (hx : x ∈ Set.univ.pi (fun i : Iic a ↦ s i)) :
    partialTraj (fun n ↦ (κ n).restrict (hs (n + 1))) a b x =
    (partialTraj κ a b x).restrict (Set.univ.pi (fun i ↦ s i)) := by
  induction b, hab using Nat.le_induction with
  | base =>
    simp only [partialTraj_self, id_apply]
    classical
    rw [restrict_dirac', if_pos hx]
    exact MeasurableSet.univ_pi fun i ↦ hs ↑i
  | succ b hab hb =>
    ext t ht
    rw [partialTraj_succ_eq_comp hab, Kernel.comp_apply' _ _ _ ht, hb, Measure.restrict_apply ht,
      partialTraj_succ_eq_comp hab, Kernel.comp_apply',
      ← lintegral_add_compl (μ := partialTraj κ a b x) _ (.univ_pi fun i ↦ hs i),
      ← add_zero (∫⁻ _, _ ∂_)]
    · have m_inter_t_pi := (ht.inter (MeasurableSet.univ_pi fun i ↦ hs i))
      congrm ?_ + ?_
      · refine setLIntegral_congr_fun (.univ_pi fun i ↦ hs i) fun y hy ↦ ?_
        simp_rw [partialTraj_succ_self]
        rw [Kernel.map_apply', Kernel.id_prod_apply', Kernel.map_apply', Kernel.restrict_apply',
          Kernel.map_apply', Kernel.id_prod_apply', Kernel.map_apply']
        · congr
          ext z
          change _ ↔
            IicProdIoc b (b + 1) (y, MeasurableEquiv.piSingleton b z) ∈ Set.univ.pi (fun _ ↦ s _)
          simp only [MeasurableEquiv.piSingleton, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk,
            Set.mem_pi, Set.mem_univ, IicProdIoc, forall_const, Subtype.forall, mem_Iic]
          constructor
          · intro h i hi
            split_ifs with h'
            · simp only [Set.mem_pi, Set.mem_univ, forall_const, Subtype.forall, mem_Iic] at hy
              exact hy i h'
            obtain rfl : i = b + 1 := by omega
            exact h
          · intro h
            convert h (b + 1) le_rfl
            simp
        any_goals fun_prop
        · exact measurableSet_apply (by fun_prop) <| measurableSet_apply (by fun_prop) m_inter_t_pi
        · exact measurableSet_apply (by fun_prop) m_inter_t_pi
        · exact m_inter_t_pi
        · refine (MeasurableEquiv.piSingleton b).measurableSet_preimage.mpr ?_
          exact measurableSet_apply (by fun_prop) <| measurableSet_apply (by fun_prop) ht
        · exact measurableSet_apply (by fun_prop) <| measurableSet_apply (by fun_prop) ht
        · exact measurableSet_apply (by fun_prop) ht
        · exact ht
      · symm
        apply setLIntegral_eq_zero
        · exact .compl (.univ_pi fun _ ↦ hs _)
        intro y hy
        simp only [Pi.zero_apply]
        rw [partialTraj_succ_self, Kernel.map_apply', Kernel.id_prod_apply', Kernel.map_apply']
        · convert measure_empty
          · ext z
            simp only [MeasurableEquiv.piSingleton, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk,
              Set.preimage_inter, Set.mem_inter_iff, Set.mem_preimage, Set.mem_pi, Set.mem_univ,
              IicProdIoc, forall_const, Subtype.forall, mem_Iic, Set.mem_empty_iff_false, iff_false,
              not_and, not_forall]
            intro h1
            simp only [Set.mem_compl_iff, Set.mem_pi, Set.mem_univ, forall_const, Subtype.forall,
              mem_Iic, not_forall] at hy
            obtain ⟨i, hi1, hi2⟩ := hy
            refine ⟨i, by omega, ?_⟩
            simpa [hi1]
          infer_instance
        · exact (MeasurableEquiv.piSingleton b).measurable
        · suffices Measurable (IicProdIoc b (b + 1) ∘ (Prod.mk y)) from
            this m_inter_t_pi
          fun_prop
        · suffices Measurable (IicProdIoc b (b + 1)) from
            this m_inter_t_pi
          fun_prop
        · fun_prop
        · exact m_inter_t_pi
    · exact ht.inter (.univ_pi fun _ ↦ hs _)

end ProbabilityTheory

open Set

variable {α : Type*} [MeasurableSpace α]
  (κ₁ κ₂ : (n : ℕ) → Kernel (Π _ : Finset.Iic n, α) α)
  [∀ n, IsMarkovKernel (κ₁ n)] [∀ n, IsMarkovKernel (κ₂ n)]
  {s : Set α} (hs : MeasurableSet s)
  (h : ∀ n, (univ.pi (fun _ => s)).EqOn (fun a => κ₁ n a) (fun a => κ₂ n a))

example {a b : ℕ} (hab : a ≤ b) : ∀ e ∈ univ.pi (fun _ => s),
    (Kernel.partialTraj (X := fun _ => α) κ₁ a b e).restrict (univ.pi (fun _ => s)) =
    (Kernel.partialTraj (X := fun _ => α) κ₂ a b e).restrict (univ.pi (fun _ => s)) := by

  intro e he
  rw [← Kernel.partialTraj_restrict (fun _ => hs) hab he,
    ← Kernel.partialTraj_restrict (fun _ => hs) hab he]
  induction b, hab using Nat.le_induction with
  | base => simp
  | succ b hab hb =>
    simp only [Kernel.partialTraj_succ_eq_comp hab, comp_apply]
    rw [hb]
    ext t ht
    rw [Measure.bind_apply ht (Kernel.aemeasurable _),
      Measure.bind_apply ht (Kernel.aemeasurable _),
      Kernel.partialTraj_restrict (fun _ => hs) hab he]
    suffices (univ.pi (fun _ => s)).EqOn
        (fun a => partialTraj (X := fun _ => α) (fun n ↦ (κ₁ n).restrict hs) b (b + 1) a t)
        (fun a => partialTraj (X := fun _ => α) (fun n ↦ (κ₂ n).restrict hs) b (b + 1) a t) by
      rw [setLIntegral_congr_fun (MeasurableSet.univ_pi fun i ↦ hs) this]
    intro a a_mem
    simp only [partialTraj_succ_self]
    rw [Kernel.map_apply' _ (by exact measurable_IicProdIoc),
      Kernel.map_apply' _ (by exact measurable_IicProdIoc),
      Kernel.id_prod_apply', Kernel.id_prod_apply',
      Kernel.map_apply', Kernel.map_apply',
      Kernel.restrict_apply', Kernel.restrict_apply']
    simp_rw [h b a_mem]
    any_goals fun_prop
    any_goals exact measurableSet_apply (by fun_prop) <| measurableSet_apply (by fun_prop)
      <| measurableSet_apply (measurable_IicProdIoc) ht
    · exact measurableSet_apply (by fun_prop) <| measurableSet_apply (measurable_IicProdIoc) ht
    · exact measurableSet_apply (by fun_prop) <| measurableSet_apply (measurable_IicProdIoc) ht
    any_goals exact measurableSet_apply (measurable_IicProdIoc) ht
    any_goals exact ht

The proofs are messy but they work! Thanks a lot again!

[Etienne Marion]

You're welcome! The lemma you added is MeasurableSet.preimage.