mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
c : α
t : Set (β × Ω)
a✝ : MeasurableSet t
⊢ Measurable (Prod.map id e)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ AEMeasurable (f ∘ Y) μ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ AEMeasurable (Prod.map id f) (Measure.map (fun x ↦ (X x, Y x)) μ)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ AEMeasurable (fun x ↦ (X x, Y x)) μ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ AEMeasurable (f ∘ X) μ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ AEMeasurable (fun a ↦ (a, f a)) (Measure.map X μ)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X✝ : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
X : α → β
c : Ω
⊢ Measurable fun x ↦ c

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst✝ : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable X (Measure.map f ν)
hY : AEMeasurable Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ AEMeasurable (Y ∘ f) ν

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst✝ : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable X (Measure.map f ν)
hY : AEMeasurable Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ AEMeasurable (fun x ↦ (X x, Y x)) (Measure.map f ν)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable Prod.fst (μ.prod ν)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  ⇑(condDistrib Y X (Measure.map Prod.fst (μ.prod ν))) =ᵐ[Measure.map (X ∘ Prod.fst) (μ.prod ν)]
    ⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν))
⊢ AEMeasurable Prod.fst (μ.prod ν)

Tactic:
fun_prop

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
⊢ (fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩) ((fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩)) x) i =
    x i

Tactic:
by
    by_cases hi : i.1 ≤ a <;> simp [hi]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable Prod.snd (ν.prod μ)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ MeasurableSet (Prod.map id (embeddingReal Ω) ⁻¹' s)

Tactic:
· exact measurable_id.prodMap hf.measurable hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  ⇑(condDistrib Y X (Measure.map Prod.snd (ν.prod μ))) =ᵐ[Measure.map (X ∘ Prod.snd) (ν.prod μ)]
    ⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ))
⊢ AEMeasurable Prod.snd (ν.prod μ)

Tactic:
fun_prop

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))
hab : a ≤ b
⊢ partialTraj κ a b =
    Nat.leRec Kernel.id
      (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1))) hab

Tactic:
obtain rfl | hab := eq_or_lt_of_le hab

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab : a ≤ a
⊢ partialTraj κ a a =
    Nat.leRec Kernel.id
      (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1))) hab

case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hab : a < b
⊢ partialTraj κ a b =
    Nat.leRec Kernel.id
      (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1))) hab✝
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
x : ℝ≥0∞
hx : x ∈ Iio ((κ a) univ + 1)
⊢ x < (κ a) univ + 1

pp: case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ (κ a) univ ∈ Iio ((κ a) univ + 1)

Tactic:
· simpa using hx

Goal state after:
case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ (κ a) univ ∈ Iio ((κ a) univ + 1)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

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

Goal state before:
pp: case inl.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable Prod.fst

Tactic:
fun_prop

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

Goal state before:
pp: case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)

Tactic:
fun_prop

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

Goal state before:
pp: case inr.base.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a a)

Tactic:
fun_prop

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

Goal state before:
pp: case inr.base
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

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

Goal state before:
pp: a k : ℕ
h : ¬k + 1 ≤ a
i : ↥(Iic k)
⊢ ↑i < k.succ

Tactic:
decreasing_by exact Nat.lt_succ_of_le (mem_Iic.1 i.2)

Goal state after:
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
s : Set ℕ
⊢ Measurable Set.ncard

Tactic:
fun_prop

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

Goal state before:
pp: 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)

Tactic:
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)
μ : (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

Tactic:
fun_prop

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

Goal state before:
pp: case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)

Tactic:
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 : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

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

Goal state before:
pp: case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ hJI)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
m : MeasurableSpace Ω
X : Ω → Set ι
u : Set ι
p : ↑I
P : Measure Ω
inst✝ : Countable ι
hX : IsSetBernoulli X u p P
⊢ Measurable fun x ↦ x ⊆ u

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ Measurable ⇑(piCongrLeft X { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ })

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ Var[c • X; μ | m] =ᵐ[μ] c ^ 2 • Var[X; μ | m]

Tactic:
calc
    Var[c • X; μ | m]
    _ =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m] := by
      rw [condVar]
      refine condExp_congr_ae ?_
      filter_upwards [condExp_smul (m := m) c X] with ω hω
      simp [hω, ← mul_sub, mul_pow]
    _ =ᵐ[μ] c ^ 2 • Var[X; μ | m] := condExp_smul ..

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

Goal state before:
pp: case f_meas
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (g a)

Tactic:
fun_prop

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

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (Function.uncurry fun a b ↦ ↑(g a b))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable Prod.fst

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst✝ : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X ↑i)
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ Measurable ⇑(piSingleton n)

Tactic:
fun_prop

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

Goal state before:
pp: case hg
α : 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)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ Measurable (g a)

Tactic:
fun_prop

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

Goal state before:
pp: α : 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
this : Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)
⊢ Measurable (∑' (n : ι), Function.uncurry (f n))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable ⇑(piSingleton a)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯ ∘ _root_.IicProdIoc a (a + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a (a + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_1.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

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

Goal state before:
pp: α : 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
this : ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b ↦ f n a b) b ∂κ a
n : ι
⊢ AEMeasurable (fun b ↦ f n a b) ((κ a).restrict s)

Tactic:
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)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
f_eq : ∀ (x : (n : ℕ) → X n) (n : ℕ), lmarginalPartialTraj κ k (a n) (f n) x = lmarginalPartialTraj κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (f n) x) atTop (𝓝 (lmarginalPartialTraj κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj κ k (k + 1) l (updateFinset x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
this : ∫⁻ (x : X (k + 1)), l (update (updateFinset x_ (Iic k) y) (k + 1) x) ∂(κ k) y ≠ ∞
x : X (k + 1)
hx :
  ∫⁻ (a : X (k + 1)), l (update (updateFinset x_ (Iic k) y) (k + 1) a) ∂(κ k) y ≤
    l (update (updateFinset x_ (Iic k) y) (k + 1) x)
⊢ ∀ (i : ℕ), Measurable (lmarginalPartialTraj κ (k + 1) (a i) (f i))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hab
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
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ a ≤ n

Tactic:
fun_prop

Goal state after:
case inl.refine_2.hab
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
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ a ≤ n