awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ n).map ((Set.Ioi n).restrict (π := X)))
          (⇑(IicProdIoi (X := X) n) :
            (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) :
        (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
      x)
have this : Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
  ((⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
    Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
Tactic: have : (updateFinset · _ x) = IicProdIoi n ∘ (Prod.mk x) ∘ (Set.Ioi n).restrict := by
    ext; simp [IicProdIoi, updateFinset]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ n).map ((Set.Ioi n).restrict (π := X)))
          (⇑(IicProdIoi (X := X) n) :
            (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) :
        (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
      x)
have hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi n).restrict (π := X))
Tactic: rw [this, ← Function.comp_assoc, ← Measure.map_map, ← Measure.map_map, map_apply, prod_apply,
    map_apply, id_apply, Measure.dirac_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi n).restrict (π := X))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ n).map ((Set.Ioi n).restrict (π := X)))
          (⇑(IicProdIoi (X := X) n) :
            (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) :
        (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
      x)
have hf₁ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((a : (↑(Set.Ioi n) : Type)) → X (↑a : ℕ))) (β :=
  (n : ℕ) → X n)
  (⇑(IicProdIoi (X := X) n) :
    (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
Tactic: rw [this, ← Function.comp_assoc, ← Measure.map_map, ← Measure.map_map, map_apply, prod_apply,
    map_apply, id_apply, Measure.dirac_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi n).restrict (π := X))
hf₁ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((a : (↑(Set.Ioi n) : Type)) → X (↑a : ℕ))) (β :=
    (n : ℕ) → X n)
    (⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
hg :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) (β :=
    (i : ℕ) → X i)
    (⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ n).map ((Set.Ioi n).restrict (π := X)))
          (⇑(IicProdIoi (X := X) n) :
            (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) :
        (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
      x)
have hf₂ : Measurable (α := (i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ)) (Prod.mk x)
Tactic: rw [this, ← Function.comp_assoc, ← Measure.map_map, ← Measure.map_map, map_apply, prod_apply,
    map_apply, id_apply, Measure.dirac_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi n).restrict (π := X))
hf₁ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((a : (↑(Set.Ioi n) : Type)) → X (↑a : ℕ))) (β :=
    (n : ℕ) → X n)
    (⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
hg :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) (β :=
    (i : ℕ) → X i)
    (⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
hf₂ : Measurable (α := (i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ)) (Prod.mk x)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ n).map ((Set.Ioi n).restrict (π := X)))
          (⇑(IicProdIoi (X := X) n) :
            (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) :
        (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
      x)
have hg₁ : Measurable (α := (i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ)) (β := (i : ℕ) → X i)
  ((⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
    Prod.mk x)
Tactic: rw [this, ← Function.comp_assoc, ← Measure.map_map, ← Measure.map_map, map_apply, prod_apply,
    map_apply, id_apply, Measure.dirac_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ ∫⁻ (x : (n : ℕ) → X n), f x ∂(traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ =
    ∫⁻ (x : (n : ℕ) → X n),
      f
        (updateFinset (π := X) x (Iic a)
          x₀) ∂(traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀
have hf : AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
  (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
Tactic: nth_rw 1 [← traj_map_updateFinset, MeasureTheory.lintegral_map']
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
hf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
⊢ ∫⁻ (x : (n : ℕ) → X n), f x ∂(traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ =
    ∫⁻ (x : (n : ℕ) → X n),
      f
        (updateFinset (π := X) x (Iic a)
          x₀) ∂(traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀
have hg : AEMeasurable (β := (n : ℕ) → X n) (_m := MeasurableSpace.pi (X := X))
  (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
  ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: nth_rw 1 [← traj_map_updateFinset, MeasureTheory.lintegral_map']
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
have h : Eq.{u_1 + 1} (α := autoParam (Measure ((n : ℕ) → X n)) AEMeasurable._auto_1)
  (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
  ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: convert! mf
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ ∀ᵐ (x :
    (i : ℕ) →
      X
        i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
      Measure ((n : ℕ) → X n)),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
have rw : ∀
  (i_f :
    (∀ᵐ (y :
        (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 : ℕ))),
        @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
      @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
        (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
          @integral _ _ _ _ (MeasurableSpace.pi (X := X))
            ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
            fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
        ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)),
  ∀ᵐ (x :
    (i : ℕ) →
      X
        i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
      Measure ((n : ℕ) → X n)),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
Tactic: rw [← traj_comp_partialTraj hab, integrable_comp_iff] at i_f
Cleared hypotheses: i_f
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
rw :
  ∀
    (i_f :
      (∀ᵐ (y :
          (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 : ℕ))),
          @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
            ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
        @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
          (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
            @integral _ _ _ _ (MeasurableSpace.pi (X := X))
              ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
              fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
          ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
            x₀)),
    ∀ᵐ (x :
      (i : ℕ) →
        X
          i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
        Measure ((n : ℕ) → X n)),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
⊢ ∀ᵐ (x :
    (i : ℕ) →
      X
        i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
      Measure ((n : ℕ) → X n)),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
have hf : ∀
  (i_f :
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
        x₀)),
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: rw [← traj_comp_partialTraj hab, integrable_comp_iff] at i_f
Cleared hypotheses: i_f
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (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 : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
⊢ ∀ᵐ (x :
    (i : ℕ) →
      X
        i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
      Measure ((n : ℕ) → X n)),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
have hf : AEMeasurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (_m := MeasurableSpace.pi (X := X))
  (frestrictLe (π := X) b) ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: apply ae_of_ae_map (p := fun x ↦ Integrable f (traj κ b x))
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (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 : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
hf :
  AEMeasurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (_m := MeasurableSpace.pi (X := X))
    (frestrictLe (π := X) b) ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ ∀ᵐ (x :
    (i : ℕ) →
      X
        i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
      Measure ((n : ℕ) → X n)),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
have h : ∀ᵐ (y :
  (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₀),
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
Tactic: apply ae_of_ae_map (p := fun x ↦ Integrable f (traj κ b x))
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (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 : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
hf :
  AEMeasurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (_m := MeasurableSpace.pi (X := X))
    (frestrictLe (π := X) b) ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
h :
  ∀ᵐ (y :
    (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₀),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
⊢ ∀ᵐ (x :
    (i : ℕ) →
      X
        i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
      Measure ((n : ℕ) → X n)),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
have apply : MeasurableSpace ((i : ↥(Iic b)) → X (↑i : ℕ))
Tactic: apply ae_of_ae_map (p := fun x ↦ Integrable f (traj κ b x))