mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measure.map I.restrict ν = μ I

Tactic:
rw [← restrict₂_comp_restrict this, ← Measure.map_map, ← frestrictLe, h (le_max_right _ _), ← hμ]

Goal state after:
case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (restrict₂ this)

case hf
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (Iic (max (I.sup id) a)).restrict
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: V : Type u_1
p : ↑I
inst✝ : Countable V
⊢ ∀ᵐ (a : Set (Sym2 V)) ∂setBer(Sym2.diagSetᶜ, p), a ∈ Set.range edgeSet

Tactic:
filter_upwards [setBernoulli_ae_subset] with S hS

Goal state after:
V : Type u_1
p : ↑I
inst✝ : Countable V
S : Set (Sym2 V)
hS : S ⊆ Sym2.diagSetᶜ
⊢ S ∈ Set.range edgeSet
Module: Mathlib.Probability.CondVar

Goal state before:
pp: case inl
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
⊢ Var[fun x ↦ 0; μ | m] = 0

pp: case inr
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
⊢ Var[fun x ↦ c; μ | m] = 0

Tactic:
· simp [← Pi.zero_def]

Goal state after:
case inr
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
⊢ Var[fun x ↦ c; μ | m] = 0
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (μ[X ^ 2 | m] - μ[X | m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), μ[X | m] x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
      exact (hX.condExp one_le_two).integrable_sq

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ Measurable (Function.uncurry fun a x ↦ f a x - g a x)

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ κ.withDensity ((fun a x ↦ f a x - g a x) + g) = κ.withDensity f

Tactic:
· exact hf.sub hg

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ κ.withDensity ((fun a x ↦ f a x - g a x) + g) = κ.withDensity f
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
b : β
⊢ (∑' (n : ι), f n) a b = ∑' (n : ι), (fun b ↦ f n a b) b

Tactic:
rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ ((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a (n + 1)).map (restrict₂ ⋯)) x₀ =
    (const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x₀

Tactic:
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 lia), 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 lia

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯) (map (frestrictLe (I.sup id)) (infinitePiNat μ)) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

pp: case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (restrict₂ ⋯)

pp: case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (Iic (I.sup id)).restrict

pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ MeasurableSpace ((i : ↥(Iic (I.sup id))) → X ↑i)

Tactic:
infinitePiNat,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯)
      (map (frestrictLe (I.sup id))
        (⇑(traj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) 0) ∘ₘ Measure.pi fun i ↦ μ ↑i)) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (restrict₂ ⋯)

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (Iic (I.sup id)).restrict

X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ MeasurableSpace ((i : ↥(Iic (I.sup id))) → X ↑i)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯)
      (⇑((Kernel.id ×ₖ const ((i : ↥(Iic 0)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)).map (_root_.IicProdIoc 0 (I.sup id))) ∘ₘ
        Measure.pi fun i ↦ μ ↑i) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

pp: case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (frestrictLe (I.sup id))

pp: case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (restrict₂ ⋯)

pp: case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (Iic (I.sup id)).restrict

Tactic:
← map_comp,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯)
      (map (_root_.IicProdIoc 0 (I.sup id))
        (⇑(Kernel.id ×ₖ const ((i : ↥(Iic 0)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) ∘ₘ Measure.pi fun i ↦ μ ↑i)) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (_root_.IicProdIoc 0 (I.sup id))

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (frestrictLe (I.sup id))

case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (restrict₂ ⋯)

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (Iic (I.sup id)).restrict
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
· exact measurable_rnDeriv κ η

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
⊢ (if h : i ≤ b then if h : i ≤ a then x₀ i else x✝ ⟨i, ⋯⟩ else x₀ i) = if h : a < i ∧ i ≤ b then x✝ ⟨i, ⋯⟩ else x₀ i

Tactic:
split_ifs <;> try rfl

Goal state after:
case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝² : i ≤ b
h✝¹ : i ≤ a
h✝ : a < i ∧ i ≤ b
⊢ x₀ i = x✝ ⟨i, ⋯⟩

case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝² : i ≤ b
h✝¹ : ¬i ≤ a
h✝ : ¬(a < i ∧ i ≤ b)
⊢ x✝ ⟨i, ⋯⟩ = x₀ i

case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝¹ : ¬i ≤ b
h✝ : a < i ∧ i ≤ b
⊢ x₀ i = x✝ ⟨i, ⋯⟩
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
⊢ f a =ᵐ[η a] ∂κ a/∂η a

Tactic:
have : κ a = ξ a + (η a).withDensity (f a) := by
    rw [h, add_apply, η.withDensity_apply hf, add_comm]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
this : κ a = ξ a + (η a).withDensity (f a)
⊢ f a =ᵐ[η a] ∂κ a/∂η a
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
⊢ ξ a = (κ a).singularPart (η a)

Tactic:
have : κ a = ξ a + (η a).withDensity (f a) := by
    rw [h, add_apply, η.withDensity_apply hf, add_comm]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
this : κ a = ξ a + (η a).withDensity (f a)
⊢ ξ a = (κ a).singularPart (η a)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∫⁻ (x : γ), κ.rnDeriv η a x ∂η a ≤ κ.bound

Tactic:
· exact measurable_rnDeriv κ η

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∫⁻ (x : γ), κ.rnDeriv η a x ∂η a ≤ κ.bound
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c✝ : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hcb : c ≤ b
⊢ f = lmarginalPartialTraj κ b d f

Tactic:
hf.lmarginalPartialTraj_of_le d mf (hac.trans hcb)

Goal state after:
case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c✝ : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hcb : c ≤ b
⊢ f = f
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
k : ℕ
hk : n ≤ k
⊢ (η.map (frestrictLe k)) x = (partialTraj κ a k) x

Tactic:
hη k hk

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
k : ℕ
hk : n ≤ k
⊢ (partialTraj κ a k) x = (partialTraj κ a k) x
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
x : 𝓧
hx : ((Kernel.boolKernel μ ν)†π) x = π.withDensity fun ω ↦ (∂(Kernel.boolKernel μ ν) ω/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
⊢ (((Kernel.boolKernel μ ν)†π) x) {false} = π {false} * (∂μ/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
rw [hx]

Goal state after:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
x : 𝓧
hx : ((Kernel.boolKernel μ ν)†π) x = π.withDensity fun ω ↦ (∂(Kernel.boolKernel μ ν) ω/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
⊢ (π.withDensity fun ω ↦ (∂(Kernel.boolKernel μ ν) ω/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x) {false} =
    π {false} * (∂μ/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
x : 𝓧
hx : ((Kernel.boolKernel μ ν)†π) x = π.withDensity fun ω ↦ (∂(Kernel.boolKernel μ ν) ω/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
⊢ (((Kernel.boolKernel μ ν)†π) x) {true} = π {true} * (∂ν/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
rw [hx]

Goal state after:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
x : 𝓧
hx : ((Kernel.boolKernel μ ν)†π) x = π.withDensity fun ω ↦ (∂(Kernel.boolKernel μ ν) ω/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
⊢ (π.withDensity fun ω ↦ (∂(Kernel.boolKernel μ ν) ω/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x) {true} =
    π {true} * (∂ν/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case e_f.hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

Tactic:
exact ms.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case e_f.hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet (Prod.mk x ⁻¹' s)

Tactic:
exact ms.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

Tactic:
exact ms.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact ms.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable fun x ↦ (frestrictLe b x, x)

Tactic:
exact ms.preimage (by fun_prop)

Goal state after:
case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable fun x ↦ (frestrictLe b x, x)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact ms.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
hf : (fun x ↦ (frestrictLe b x, x (b + 1))) = (Prod.map id fun x ↦ x (b + 1)) ∘ fun x ↦ (frestrictLe b x, x)
⊢ (partialTraj κ a b) x₀ ⊗ₘ κ b = Measure.map (Prod.map id fun x ↦ x (b + 1)) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)

Tactic:
← Measure.compProd_map (by fun_prop),

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
hf : (fun x ↦ (frestrictLe b x, x (b + 1))) = (Prod.map id fun x ↦ x (b + 1)) ∘ fun x ↦ (frestrictLe b x, x)
⊢ (partialTraj κ a b) x₀ ⊗ₘ κ b = (partialTraj κ a b) x₀ ⊗ₘ (traj κ b).map fun x ↦ x (b + 1)
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n : ℕ
p : ↑I
k : ℕ
⊢ Bin(n, p) {k} = (∑ k ≤ n, ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k}

Tactic:
rw [binomial_singleton, finsetSum_apply, Finset.sum_eq_single k]

Goal state after:
n : ℕ
p : ↑I
k : ℕ
⊢ ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) =
    (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k}

case h₀
n : ℕ
p : ↑I
k : ℕ
⊢ ∀ b ∈ Finset.Iic n, b ≠ k → (ENNReal.ofReal (↑(n.choose b) * ↑p ^ b * (1 - ↑p) ^ (n - b)) • dirac b) {k} = 0

case h₁
n : ℕ
p : ↑I
k : ℕ
⊢ k ∉ Finset.Iic n → (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k} = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
⊢ p a ≤ 1

Tactic:
refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)

Goal state after:
α : Type u_1
p : PMF α
a b : α
⊢ (if b = a then p a else 0) ≤ p b
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞

Tactic:
· refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : 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 ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
⊢ ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x) =
    ∫ (x_1 : (n : ℕ) → X n),
      ((traj κ a) x₀)[f | ↑piLE c] (updateFinset x (Iic c) (frestrictLe c x_1)) ∂(traj κ b) (frestrictLe b x)

Tactic:
congr with y
    apply stronglyMeasurable_condExp.dependsOn_of_piLE
    simp only [Set.mem_Iic, updateFinset, mem_Iic, frestrictLe_apply, dite_eq_ite]
    exact fun i hi ↦ (if_pos hi).symm

Goal state after: