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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
⊢ ((ν ⊗ₖ IsCondKernelCDF.toKernel f hf) a) s = (κ a) s

Tactic:
Kernel.compProd_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' s) ∂ν a = (κ a) s
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_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop (𝓝 ((κ.fst a).real univ))

Tactic:
fst_real_apply _ _ MeasurableSet.univ

Goal state after:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop
    (𝓝 ((κ a).real {p | p.1 ∈ univ}))
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case 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 ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun x ↦ κ.densityProcess ν j a x s) (ν a)

Tactic:
exact integrable_densityProcess hκν j a 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ μ (X ⁻¹' s) = (Measure.map (fun x ↦ (X x, Y x)) μ).fst s

Tactic:
Measure.fst_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ μ (X ⁻¹' s) = (Measure.map (fun x ↦ (X x, Y x)) μ) (Prod.fst ⁻¹' s)
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 X (Measure.map Prod.fst (μ.prod ν))

Tactic:
by simpa

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 Y (Measure.map Prod.fst (μ.prod ν))

Tactic:
by simpa

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 X (Measure.map Prod.fst (μ.prod ν))

Tactic:
by simpa

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 X (Measure.map Prod.snd (ν.prod μ))

Tactic:
by simpa

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 Y (Measure.map Prod.snd (ν.prod μ))

Tactic:
by simpa

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 X (Measure.map Prod.snd (ν.prod μ))

Tactic:
by simpa

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

Goal state before:
pp: case iUnion.hn
α : 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
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), ∫ (x : γ) in f i, κ.density ν a x s ∂ν a = (κ a).real (f i ×ˢ s)
⊢ Pairwise (Function.onFun Disjoint fun i ↦ f i ×ˢ s)

pp: case iUnion.h
α : 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
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), ∫ (x : γ) in f i, κ.density ν a x s ∂ν a = (κ a).real (f i ×ˢ s)
⊢ ∀ (i : ℕ), MeasurableSet (f i ×ˢ s)

Tactic:
· exact hf_disj.mono fun _ _ h ↦ h.set_prod_left _ _

Goal state after:
case iUnion.h
α : 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
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), ∫ (x : γ) in f i, κ.density ν a x s ∂ν a = (κ a).real (f i ×ˢ s)
⊢ ∀ (i : ℕ), MeasurableSet (f i ×ˢ s)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

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

Tactic:
rw [Nat.leRec_succ, ← partialTraj_le_def]; lia

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 κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (x : γ) ∂κ.fst a, Tendsto (fun m ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)

Tactic:
by
  refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
  · exact fun m ↦ integrable_density le_rfl _ (hseq_meas m)
  · rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]
    convert! tendsto_integral_density_of_monotone (κ := κ) le_rfl a seq hseq hseq_iUnion hseq_meas
    simp only [measureReal_def]
    rw [fst_apply' _ _ MeasurableSet.univ]
    simp only [mem_univ, ofPred_true]
  · exact ae_of_all _ (fun c n m hnm ↦ density_mono_set le_rfl a c (hseq hnm))
  · exact ae_of_all _ (fun x m ↦ density_le_one le_rfl a x (seq m))

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

Goal state before:
pp: ι : Type u_1
u : Set ι
inst✝ : Countable ι
s : Set ι
p : ↑I
hs : ¬s ⊆ u
⊢ {s} ⊆ {x | (fun s ↦ s ⊆ u) x}ᶜ

Tactic:
by simpa

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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
l : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
hl : ∀ (k : ℕ) (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 (l k x))
x y : (i : ℕ) → X i
this :
  Tendsto (fun n ↦ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)) atTop
    (𝓝 (l p (updateFinset x (Iic p) x₀)))
⊢ l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) x₀)

Tactic:
exact tendsto_nhds_unique this (hl p _)

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 : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
⊢ lmarginalPartialTraj κ b c f = f

Tactic:
by
  ext x
  rw [lmarginalPartialTraj_eq_lintegral_map mf]
  refine @lintegral_eq_const _ _ _ ?_ _ _ (ae_of_all _ fun y ↦ hf fun i hi ↦ ?_)
  · refine @IsMarkovKernel.isProbabilityMeasure _ _ _ _ _ ?_ _
    exact IsMarkovKernel.map _ (by fun_prop)
  · simp_all only [coe_Iic, Set.mem_Iic, Function.updateFinset, mem_Ioc, dite_eq_right_iff]
    lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic (swap α β)

Tactic:
unfold swap; infer_instance

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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ ((traj κ a).map (frestrictLe b)) x = (partialTraj κ a b) x

Tactic:
traj_map_frestrictLe

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 : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ (partialTraj κ a b) x = (partialTraj κ a b) x
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac✝ : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
ω : Ω
h_ac : κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∫⁻ (y : 𝓧) in t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω y ∂⇑κ ∘ₘ μ = (κ ω) t

Tactic:
change ∫⁻ x in t, κ.rnDeriv (Kernel.const Ω (κ ∘ₘ μ)) ω x ∂(Kernel.const Ω (κ ∘ₘ μ) ω) = _

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac✝ : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
ω : Ω
h_ac : κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∫⁻ (x : 𝓧) in t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x ∂(Kernel.const Ω (⇑κ ∘ₘ μ)) ω = (κ ω) t
Module: Mathlib.Probability.Decision.Risk.Countable

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Countable 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
⊢ avgRisk ℓ P κ π = ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * (⇑κ ∘ₘ P θ) {y} ∂π

Tactic:
by
  simp only [avgRisk, lintegral_countable']
  rw [lintegral_tsum]
  · rfl
  · refine fun y ↦ Measurable.aemeasurable ?_
    exact Measurable.mul (by fun_prop) ((κ ∘ₖ P).measurable_coe (measurableSet_singleton y))

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∈ s
hy : y ∈ s
⊢ Ber(x, y, p).real s = 1

Tactic:
by
  classical
  simp_all [bernoulliMeasure_real_apply]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∈ s
hy : y ∉ s
⊢ Ber(x, y, p).real s = ↑p

Tactic:
by
  classical
  simp_all [bernoulliMeasure_real_apply]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∉ s
hy : y ∈ s
⊢ Ber(x, y, p).real s = 1 - ↑p

Tactic:
by
  classical
  simp_all [bernoulliMeasure_real_apply]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∉ s
hy : y ∉ s
⊢ Ber(x, y, p).real s = 0

Tactic:
by
  classical
  simp_all [bernoulliMeasure_real_apply]

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 < (↑α).re

Tactic:
by simpa

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 < (↑β).re

Tactic:
by simpa

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

Goal state before:
pp: case hfm
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ AEStronglyMeasurable (fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (volume.restrict (Ioo 0 1))

Tactic:
· exact Measurable.aestronglyMeasurable (by fun_prop)

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
h : MeasurableSingletonClass α
⊢ (Measure.dirac a).toPMF = pure a

Tactic:
toPMF_eq_iff_toMeasure_eq,

Goal state after:
α : Type u_1
a : α
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
h : MeasurableSingletonClass α
⊢ Measure.dirac a = (pure a).toMeasure
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ (p.filter s h) a = 0 ↔ a ∉ s ∨ a ∉ p.support

Tactic:
apply_eq_zero_iff,

Goal state after:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ a ∉ (p.filter s h).support ↔ a ∉ s ∨ a ∉ p.support
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞

Tactic:
by_cases h_top : κ a t = ∞

Goal state after:
case pos
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
h_top : (κ a) t = ∞
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞

case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
h_top : ¬(κ a) t = ∞
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure ((condExpKernel μ m) a)
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ω : Ω
hω_eq : ((condExpKernel μ m) ω).real t = μ[t.indicator fun ω ↦ 1 | m] ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ ((condExpKernel μ m) ω) t = 0 ∨ (((condExpKernel μ m) ω) t).toReal = 1

Tactic:
ENNReal.toReal_eq_one_iff

Goal state after:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure ((condExpKernel μ m) a)
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ω : Ω
hω_eq : ((condExpKernel μ m) ω).real t = μ[t.indicator fun ω ↦ 1 | m] ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
inst✝¹ : StandardBorelSpace Ω
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : ((condExpKernel μ m) ω).real t = μ[t.indicator fun ω ↦ 1 | m] ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ ((condExpKernel μ m) ω) t = 0 ∨ (((condExpKernel μ m) ω) t).toReal = 1

Tactic:
ENNReal.toReal_eq_one_iff

Goal state after:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
inst✝¹ : StandardBorelSpace Ω
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : ((condExpKernel μ m) ω).real t = μ[t.indicator fun ω ↦ 1 | m] ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ ((κ₁.hom ∥ₖ κ₂.hom ∥ₖ η.hom) a✝) (⇑prodAssoc ⁻¹' s✝) = ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝

Tactic:
Kernel.parallelComp_apply

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom ∥ₖ κ₂.hom) a✝.1).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) = ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom ∥ₖ κ₂.hom) a✝.1).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) = ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝

Tactic:
Kernel.parallelComp_apply

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom a✝.1.1).prod (κ₂.hom a✝.1.2)).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) =
    ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝