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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ AEMeasurable (fun b ↦ ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)) (ν a)

Tactic:
refine (Measurable.ennreal_ofReal ?_).aemeasurable
    exact (measurable_stieltjesOfMeasurableRat hf.measurable x).comp measurable_prodMk_left

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd ↑r).real s

Tactic:
setLIntegral_preCDF_fst _ _ hs,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ((ρ.IicSnd ↑r) s).toReal = (ρ.IicSnd ↑r).real s
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
t : β
⊢ Monotone (f (a, t)) → Antitone fun i ↦ f (a, t) (seq i)

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
t : β
ht : Monotone (f (a, t))
⊢ Antitone fun i ↦ f (a, t) (seq i)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
t : β
⊢ Monotone (f (a, t)) → Monotone fun i ↦ f (a, t) (seq i)

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
t : β
ht : Monotone (f (a, t))
⊢ Monotone fun i ↦ f (a, t) (seq i)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n ↦ f (a, t) ↑n) atTop (𝓝 1)
t : β
⊢ Tendsto (fun n ↦ f (a, t) ↑n) atTop (𝓝 1) → Monotone (f (a, t)) → Tendsto (f (a, t)) atTop (𝓝 1)

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n ↦ f (a, t) ↑n) atTop (𝓝 1)
t : β
ht : Tendsto (fun n ↦ f (a, t) ↑n) atTop (𝓝 1)
⊢ Monotone (f (a, t)) → Tendsto (f (a, t)) atTop (𝓝 1)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)
t : β
⊢ Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0) → Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)
⊢ Tendsto (f (a, t)) atBot (𝓝 0)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n ↦ f (a, t) (-↑n)) atTop (𝓝 0)
t : β
⊢ Tendsto (fun n ↦ f (a, t) (-↑n)) atTop (𝓝 0) → Monotone (f (a, t)) → Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n ↦ f (a, t) (-↑n)) atTop (𝓝 0)
t : β
ht : Tendsto (fun n ↦ f (a, t) (-↑n)) atTop (𝓝 0)
⊢ Monotone (f (a, t)) → Tendsto (fun q ↦ f (a, t) (-q)) atTop (𝓝 0)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
⊢ IsPreBrownianReal (fun t ω ↦ (√↑c)⁻¹ * B (c * t) ω) P

Tactic:
refine IsGaussianProcess.isPreBrownianReal_of_covariance ?_ (fun t ↦ ?_) (fun s t hst ↦ ?_)
  · have this t ω : (√c)⁻¹ * B (c * t) ω = (√c)⁻¹ • ((B ∘ (c * ·)) t ω) := rfl
    simp_rw [this]
    exact (hB.isGaussianProcess.comp_right _).smul _
  · rw [integral_const_mul, hB.integral_eval, mul_zero]
  · rw [covariance_const_mul_left, covariance_const_mul_right, hB.covariance_eval, min_eq_left]
    · simp [field]
    · exact mul_le_mul_right hst c

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ ∫ (c : β) in A, f (a, c) ↑r ∂ν a

Tactic:
refine setIntegral_mono_ae ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ IntegrableOn (fun t ↦ ⨅ r', f (a, t) ↑r') A (ν a)

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ IntegrableOn (fun c ↦ f (a, c) ↑r) A (ν a)

case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
⊢ (fun t ↦ ⨅ r', f (a, t) ↑r') ≤ᵐ[ν a] fun c ↦ f (a, c) ↑r
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
t : β
⊢ (∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)) → ⨅ r', f (a, t) ↑r' ≤ f (a, t) ↑r

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : ↑(Ioi q)
t : β
ht : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
⊢ ⨅ r', f (a, t) ↑r' ≤ f (a, t) ↑r
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∫ (c : β) in A, f (a, c) q ∂ν a ≤ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a

Tactic:
refine setIntegral_mono_ae ?_ ?_ ?_

Goal state after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ IntegrableOn (fun c ↦ f (a, c) q) A (ν a)

case refine_2.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ IntegrableOn (fun t ↦ ⨅ r, f (a, t) ↑r) A (ν a)

case refine_2.refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ (fun c ↦ f (a, c) q) ≤ᵐ[ν a] fun t ↦ ⨅ r, f (a, t) ↑r
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (κ a) {p | p.1 ∈ countablePartitionSet n x}

Tactic:
refine measure_mono (fun x ↦ ?_)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x✝ : γ
s : Set β
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ s → x ∈ {p | p.1 ∈ countablePartitionSet n x✝}
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m ↦ ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop (𝓝 0)

Tactic:
by
    let s' : ℕ → Set ℝ := fun n ↦ Iic (s n)
    refine tendsto_integral_density_of_antitone le_rfl a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)
    · refine fun i j hij ↦ Iic_subset_Iic.mpr ?_
      exact mod_cast hs_anti hij
    · ext x
      simp only [mem_iInter, mem_Iic, mem_empty_iff_false, iff_false, not_forall, not_le, s']
      rw [tendsto_atTop_atBot] at hs_tendsto
      have ⟨q, hq⟩ := exists_rat_lt x
      obtain ⟨i, hi⟩ := hs_tendsto q
      refine ⟨i, lt_of_le_of_lt ?_ hq⟩
      exact mod_cast hi i le_rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
u v : ↥S
huv : u ≠ v
⊢ (Disjoint on fun i ↦ ↑i) u v

Tactic:
simp only [Function.onFun]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
u v : ↥S
huv : u ≠ v
⊢ Disjoint ↑u ↑v
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
hxuniv : (κ x) univ = (ρ.condKernel x) univ
t : Set ℝ
⊢ MeasurableSet t → (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ

Tactic:
ht

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
hxuniv : (κ x) univ = (ρ.condKernel x) univ
t : Set ℝ
ht : MeasurableSet t
⊢ (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f ρ
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ

Tactic:
by
  conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
  rw [← ρ.disintegrate ρ.condKernel] at hf
  rw [integral_compProd hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
t : γ
⊢ Tendsto (fun n ↦ κ.densityProcess ν n a t s) atTop
      (𝓝 (Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) t)) →
    κ.density ν a t s = Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) t

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
t : γ
ht :
  Tendsto (fun n ↦ κ.densityProcess ν n a t s) atTop
    (𝓝 (Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) t))
⊢ κ.density ν a t s = Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) t
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
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)

Tactic:
by_cases hX : AEMeasurable X μ
  swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]
  refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_
  rw [Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX]
  simp [Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : γ), ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (univ ×ˢ s)

Tactic:
rw [← setLIntegral_univ]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in univ, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (univ ×ˢ s)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
⊢ MeasurableSet t →
    μ t < ∞ →
      ∫ (x : α) in t, ((condDistrib Y X μ) (X x)).real s ∂μ = ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun ω ↦ 1) x ∂μ

Tactic:
ht

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ t < ∞ → ∫ (x : α) in t, ((condDistrib Y X μ) (X x)).real s ∂μ = ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun ω ↦ 1) x ∂μ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : 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 : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m ↦ (κ a).real (univ ×ˢ seq m)) atTop (𝓝 (ENNReal.toReal 0))

Tactic:
have h_cont := ENNReal.continuousAt_toReal ENNReal.zero_ne_top

Goal state after:
α : 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 : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Tendsto (fun m ↦ (κ a).real (univ ×ˢ seq m)) atTop (𝓝 (ENNReal.toReal 0))
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
⊢ IsSFiniteKernel (partialTraj κ a b)

Tactic:
obtain hab | hba := le_total a b
  · induction b, hab using Nat.le_induction with
    | base => rw [partialTraj_self]; infer_instance
    | succ k hak => rw [partialTraj_succ_of_le hak]; infer_instance
  · rw [partialTraj_le hba]; infer_instance

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsFiniteKernel (κ n)
a b : ℕ
⊢ IsFiniteKernel (partialTraj κ a b)

Tactic:
obtain hab | hba := le_total a b
  · induction b, hab using Nat.le_induction with
    | base => rw [partialTraj_self]; infer_instance
    | succ k hak => rw [partialTraj_succ_of_le hak]; infer_instance
  · rw [partialTraj_le hba]; infer_instance

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
⊢ IsZeroOrMarkovKernel (partialTraj κ a b)

Tactic:
obtain hab | hba := le_total a b
  · induction b, hab using Nat.le_induction with
    | base => rw [partialTraj_self]; infer_instance
    | succ k hak => rw [partialTraj_succ_of_le hak]; infer_instance
  · rw [partialTraj_le hba]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
t : γ
⊢ t ∈ {x | (κ.fst a) (countablePartitionSet n x) = 0} → t ∈ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u

Tactic:
ht

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
t : γ
ht : t ∈ {x | (κ.fst a) (countablePartitionSet n x) = 0}
⊢ t ∈ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hd
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
s : Set γ
hs : s ∈ countablePartition γ n
t : Set γ
⊢ t ∈ countablePartition γ n → s ≠ t → Function.onFun Disjoint (fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u) s t

Tactic:
ht

Goal state after:
case hd
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
s : Set γ
hs : s ∈ countablePartition γ n
t : Set γ
ht : t ∈ countablePartition γ n
⊢ s ≠ t → Function.onFun Disjoint (fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u) s t
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
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
⊢ partialTraj κ a b = (Kernel.id ×ₖ (partialTraj κ a b).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b)

Tactic:
rw [partialTraj_le hba, IicProdIoc_le hba, map_comp_right, ← fst_eq, deterministic_map,
      fst_prod, id_map]
    all_goals fun_prop

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

Goal state before:
pp: case neg.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 ∨ (κ.fst a) (countablePartitionSet n x) ≠ 0

Tactic:
· exact Or.inr h0

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

Goal state before:
pp: ι : Type u_1
s u : Set ι
inst✝ : Countable ι
p : ↑I
hsu : s ⊆ u
hu : u.Finite
⊢ setBer(u, p).real {s} = ↑p ^ s.ncard * (1 - ↑p) ^ (u \ s).ncard

Tactic:
simp [measureReal_def, setBernoulli_singleton p hsu hu]

Goal state after: