awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
cylinder :
  ∀ (N : ℕ) (S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))) (mS : MeasurableSet S)
    (t_eq : t = MeasureTheory.cylinder (α := X) (Iic N) S),
    Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
      (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t

Tactic:
obtain ⟨N, S, mS, t_eq⟩ : ∃ N S, MeasurableSet S ∧ t = cylinder (Iic N) S := by
      simpa [measurableCylinders_nat] using ht
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))
mS : MeasurableSet S
t_eq : t = MeasureTheory.cylinder (α := X) (Iic N) S
cylinder :
  Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    ((Measure.map (restrict₂ (π := X) ⋯)
            ((partialTraj (X := X) κ a ((Iic N).sup id) :
                (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
              x₀) :
          Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) :
        (a : Set ((j : ↥(Iic N)) → X (↑j : ℕ))) → ℝ≥0∞)
      S
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t

Tactic:
simp_rw [trajFun, AddContent.measure_eq _ _ generateFrom_measurableCylinders.symm _ ht,
      trajContent, projectiveFamilyContent_congr _ t t_eq mS, inducedFamily]

Premises used: MeasureTheory.AddContent.measure_eq, MeasureTheory.inducedFamily, MeasureTheory.projectiveFamilyContent_congr, ProbabilityTheory.Kernel.trajContent, ProbabilityTheory.Kernel.trajFun, MeasureTheory.generateFrom_measurableCylinders, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))
mS : MeasurableSet S
t_eq : t = cylinder (α := X) (Iic N) S
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    ((Measure.map (restrict₂ (π := X) ⋯)
            ((partialTraj (X := X) κ a ((Iic N).sup id) :
                (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
              x₀) :
          Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) :
        (a : Set ((j : ↥(Iic N)) → X (↑j : ℕ))) → ℝ≥0∞)
      S

Tactic:
Measure.measurable_measure.1 ?_ _ mS

Premises used: MeasureTheory.Measure.measurable_measure, Iff.mp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))
mS : MeasurableSet S
t_eq : t = MeasureTheory.cylinder (α := X) (Iic N) S
cylinder :
  Measurable (β := Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    Measure.map (restrict₂ (π := X) ⋯)
      ((partialTraj (X := X) κ a ((Iic N).sup id) :
          (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
        x₀)
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    ((Measure.map (restrict₂ (π := X) ⋯)
            ((partialTraj (X := X) κ a ((Iic N).sup id) :
                (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
              x₀) :
          Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) :
        (a : Set ((j : ↥(Iic N)) → X (↑j : ℕ))) → ℝ≥0∞)
      S

Tactic:
refine Measure.measurable_measure.1 ?_ _ mS

Premises used: MeasureTheory.Measure.measurable_measure, Iff.mp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))
mS : MeasurableSet S
t_eq : t = cylinder (α := X) (Iic N) S
⊢ Measurable (β := Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    Measure.map (restrict₂ (π := X) ⋯)
      ((partialTraj (X := X) κ a ((Iic N).sup id) :
          (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
        x₀)

Tactic:
(Measure.measurable_map _ (measurable_restrict₂ _)).comp (measurable _)

Premises used: Measurable.comp, Finset.measurable_restrict₂, Set.Mem, MeasureTheory.Measure.measurable_map, setOf, ProbabilityTheory.Kernel.measurable
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))
mS : MeasurableSet S
t_eq : t = cylinder (α := X) (Iic N) S
⊢ Measurable (β := Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    Measure.map (restrict₂ (π := X) ⋯)
      ((partialTraj (X := X) κ a ((Iic N).sup id) :
          (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
        x₀)

Tactic:
exact (Measure.measurable_map _ (measurable_restrict₂ _)).comp (measurable _)

Premises used: Measurable.comp, Finset.measurable_restrict₂, MeasureTheory.Measure.measurable_map, ProbabilityTheory.Kernel.measurable
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
mt : MeasurableSet t
ht :
  (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    t mt
⊢ ∀ (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)), IsProbabilityMeasure (trajFun (X := X) κ a x₀)

Tactic:
have := isProbabilityMeasure_trajFun κ a
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
mt : MeasurableSet t
ht :
  (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    t mt
this : ∀ (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)), IsProbabilityMeasure (trajFun (X := X) κ a x₀)
⊢ (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    tᶜ ⋯

Tactic:
simpa [measure_compl mt (measure_ne_top _ _)] using Measurable.const_sub ht _

Premises used: MeasureTheory.measure_compl, Measurable.const_sub, MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
f : ℕ → Set ((n : ℕ) → X n)
disf : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
        Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
          (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
      (f i) ⋯
⊢ (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    (⋃ (i : ℕ), f i) ⋯

Tactic:
simpa [measure_iUnion disf mf] using Measurable.tsum hf

Premises used: Measurable.tsum, MeasureTheory.measure_iUnion
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ (traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x = trajFun (X := X) κ a x

Tactic:
rfl

Premises used: MeasureTheory.Measure.trim, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.ofMeasurable, MeasureTheory.AddContent.measure, ProbabilityTheory.Kernel.trajFun, rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ IsMarkovKernel (traj (X := X) κ a)

Tactic:
⟨fun _ ↦ isProbabilityMeasure_trajFun ..⟩

Premises used: ProbabilityTheory.Kernel.isProbabilityMeasure_trajFun, ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
h :
  ∀ (x : (i : ↥(Iic a)) → X (↑i : ℕ)) (s : Set ((i : ↥(Iic b)) → X (↑i : ℕ))),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        (((((traj (X := X) κ a).map (frestrictLe (π := X) b) :
                    (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
                  x :
                Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
              (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
                Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
              (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ (traj (X := X) κ a).map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
h_1 : MeasurableSet s
h : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
⊢ Eq (α := ℝ≥0∞)
    (((((traj (X := X) κ a).map (frestrictLe (π := X) b) :
                (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [map_apply, traj_apply, frestrictLe, isProjectiveLimit_trajFun, inducedFamily_Iic]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasureTheory.inducedFamily_Iic, ProbabilityTheory.Kernel.isProjectiveLimit_trajFun, ProbabilityTheory.Kernel.traj_apply, Preorder.frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
h : MeasurableSet s
⊢ Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
rw :
  Eq (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (((traj (X := X) κ a).map (frestrictLe (π := X) b) :
          (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        x :
      Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
rw₁ rw₂ :
  Eq (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x)

Tactic:
rw [← map_apply _ (measurable_frestrictLe b), traj_map_frestrictLe]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.traj_map_frestrictLe, Preorder.measurable_frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
rw : partialTraj (X := X) κ b a = deterministic (frestrictLe₂ (π := X) hab) ⋯
rw₁ :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic b)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) hab) ⋯) (deterministic (frestrictLe₂ (π := X) hab) ⋯)
rw₂ : a ≤ b
rw₃ :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic b)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) hab) ⋯) (deterministic (frestrictLe₂ (π := X) hab) ⋯)
rw₄ : a ≤ b
⊢ (traj (X := X) κ b).map (frestrictLe (π := X) a) = deterministic (frestrictLe₂ (π := X) hab) ⋯

Tactic:
rw [traj_map_frestrictLe, partialTraj_le]

Premises used: ProbabilityTheory.Kernel.partialTraj_le, ProbabilityTheory.Kernel.traj_map_frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      frestrictLe (π := X) (a + 1))

Tactic:
have hf : (fun x : Π n, X n ↦ x (a + 1)) =
      (fun x ↦ x ⟨a + 1, mem_Iic.2 le_rfl⟩) ∘ frestrictLe (a + 1) := rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      frestrictLe (π := X) (a + 1))
⊢ Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) (frestrictLe (π := X) (a + 1))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      frestrictLe (π := X) (a + 1))
⊢ Measurable (β := X (a + 1)) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      frestrictLe (π := X) (a + 1))
rw :
  (traj (X := X) κ a).map
      ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
        frestrictLe (π := X) (a + 1)) =
    κ a
rw₁ :
  (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
      ((traj (X := X) κ a).map (frestrictLe (π := X) (a + 1))) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) =
    κ a
rw₂ :
  (map (partialTraj (X := X) κ a (a + 1)) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) =
    κ a
rw₃ rw₄ : κ a = κ a
⊢ ((traj (X := X) κ a).map fun (x : (n : ℕ) → X n) ↦ x (a + 1)) = κ a

Tactic:
rw [hf, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe,
    map_partialTraj_succ_self]

Premises used: ProbabilityTheory.Kernel.map_partialTraj_succ_self, ProbabilityTheory.Kernel.map_comp_right, ProbabilityTheory.Kernel.traj_map_frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
h :
  ∀ (x : (i : ↥(Iic a)) → X (↑i : ℕ)),
    Eq (α := Measure ((n : ℕ) → X n))
      ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n))
⊢ η = traj (X := X) κ a

Tactic:
ext x : 1
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ Eq (α := Measure ((n : ℕ) → X n))
    ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n))

Tactic:
((isProjectiveLimit_trajFun _ _ _).unique ?_).symm

Premises used: MeasureTheory.Measure.trim, ProbabilityTheory.Kernel.isProjectiveLimit_trajFun, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.ofMeasurable, MeasureTheory.AddContent.measure, ProbabilityTheory.Kernel.trajFun, MeasureTheory.IsProjectiveLimit.unique, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
h :
  IsProjectiveLimit (α := X) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
⊢ Eq (α := Measure ((n : ℕ) → X n))
    ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n))

Tactic:
refine ((isProjectiveLimit_trajFun _ _ _).unique ?_).symm

Premises used: ProbabilityTheory.Kernel.isProjectiveLimit_trajFun, MeasureTheory.IsProjectiveLimit.unique, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
h :
  ∀ ⦃n_1 : ℕ⦄,
    n ≤ n_1 →
      Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic n_1)) → X (↑i : ℕ)))
        (Measure.map (frestrictLe (π := X) n_1) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
        (inducedFamily (X := X)
          (fun (n : ℕ) ↦
            (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
          (Iic n_1))
rw :
  IsProjectiveMeasureFamily (α := X)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
⊢ IsProjectiveLimit (α := X) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)

Tactic:
rw [isProjectiveLimit_nat_iff' _ _ n]

Premises used: MeasureTheory.isProjectiveLimit_nat_iff'