-- 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)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_cf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X))
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
mcf :
  StronglyMeasurable
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
h :
  ∀ (x : (n : ℕ) → X n)
    (h1 :
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
          ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
          (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) c) (m₀ := MeasurableSpace.pi (X := X))
            ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
          x =
        condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
          ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f x)
    (h2 :
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
          ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
          (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
            ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
          x =
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
          fun (y : (n : ℕ) → X n) ↦
          condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
            ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f y),
    condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f x =
      @integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic c)) ↦ X (↑i : ℕ)))
        ((partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
          (frestrictLe (π := X) b x))
        fun (y : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦
        condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
          ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f
          (updateFinset (π := X) x (Iic c) y)
⊢ condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      f =ᶠ[ae (F := Measure ((n : ℕ) → X n))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))]
    fun (x : (n : ℕ) → X n) ↦
    @integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic c)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x))
      fun (y : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f
        (updateFinset (π := X) x (Iic c) y)

Tactic:
filter_upwards [piLE.condExp_condExp f hbc, condExp_traj hab i_cf] with x h1 h2

Premises used: MeasureTheory.Filtration.condExp_condExp, ProbabilityTheory.Kernel.condExp_traj, MeasureTheory.Filtration.piLE