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

Goal state before:
pp: case iUnion.hn
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ Pairwise (Function.onFun Disjoint fun i ↦ s ×ˢ f i)

pp: case iUnion.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∀ (i : ℕ), MeasurableSet (s ×ˢ f i)

pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∀ (i : ℕ), AEMeasurable (fun b ↦ ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i)) ((ν a).restrict s)

Tactic:
· exact hf_disj.mono fun i j h ↦ h.set_prod_right _ _

Goal state after:
case iUnion.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∀ (i : ℕ), MeasurableSet (s ×ˢ f i)

case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∀ (i : ℕ), AEMeasurable (fun b ↦ ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i)) ((ν a).restrict 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
⊢ (Measure.map (fun a ↦ (X a, Y a)) μ).snd = Measure.map Y μ

Tactic:
Measure.snd_map_prodMk₀ hX

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 : AEMeasurable X μ
hY : AEMeasurable Y μ
⊢ Measure.map Y μ = Measure.map Y μ
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : β → E
a : α
inst✝² : CompleteSpace E
g : α → β
inst✝¹ : MeasurableSingletonClass β
hg : Measurable g
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
by
  rw [deterministic_apply, setIntegral_dirac f _ s]

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

Goal state before:
pp: case succ
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
j : ℕ
hj : j + 1 ∈ Iic a
⊢ (if h : j + 1 ≤ a then x ⟨j + 1, ⋯⟩ else ind j fun i ↦ iterateInduction x ind ↑i) = x ⟨j + 1, hj⟩

Tactic:
dif_pos (mem_Iic.1 hj)

Goal state after:
case succ
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
j : ℕ
hj : j + 1 ∈ Iic a
⊢ x ⟨j + 1, ⋯⟩ = x ⟨j + 1, hj⟩
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)
k : ℕ
x : (n : ℕ) → X n
⊢ Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x

Tactic:
intro m

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 : ℕ → 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)
k : ℕ
x : (n : ℕ) → X n
m : ℕ
⊢ ∀ ⦃b : ℕ⦄,
    m ≤ b → (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) b ≤ (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) m
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ ((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a) +
        ((η.withDensity (κ.rnDeriv η)) a) (s \ κ.mutuallySingularSetSlice η a) +
      ((κ a) (s ∩ κ.mutuallySingularSetSlice η a) + 0) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a) + (κ a) (s \ κ.mutuallySingularSetSlice η a)

Tactic:
add_zero,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ ((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a) +
        ((η.withDensity (κ.rnDeriv η)) a) (s \ κ.mutuallySingularSetSlice η a) +
      (κ a) (s ∩ κ.mutuallySingularSetSlice η a) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a) + (κ a) (s \ κ.mutuallySingularSetSlice η a)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hbc✝ : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      ∫⁻ (z_1 : (i : ↥(Iic c)) → X ↑i),
        f
          (updateFinset (updateFinset x₀ (Iic b) z) (Iic c)
            z_1) ∂(partialTraj κ b c) z ∂(partialTraj κ a b) ((Iic a).restrict x₀) =
    ∫⁻ (z : (i : ↥(Iic c)) → X ↑i), f (updateFinset x₀ (Iic c) z) ∂(partialTraj κ a c) ((Iic a).restrict x₀)

Tactic:
updateFinset_updateFinset_of_subset (Iic_subset_Iic.2 hbc.le)

Goal state after:
case inr.inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hbc✝ : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      ∫⁻ (z : (i : ↥(Iic c)) → X ↑i),
        f (updateFinset x₀ (Iic c) z) ∂(partialTraj κ b c) z ∂(partialTraj κ a b) ((Iic a).restrict x₀) =
    ∫⁻ (z : (i : ↥(Iic c)) → X ↑i), f (updateFinset x₀ (Iic c) z) ∂(partialTraj κ a c) ((Iic a).restrict x₀)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
x✝¹ : ι → κ → X
x✝ : (_ : ι) × κ
⊢ (⇑(piCongrLeft (fun x ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘ ⇑(MeasurableEquiv.curry ι κ X).symm) x✝¹ x✝ =
    (piCurry fun x x_1 ↦ X).symm x✝¹ x✝

Tactic:
simp [piCongrLeft, Equiv.piCongrLeft, Sigma.uncurry]

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

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : ↑I
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ ∀ᵐ (x : ℕ) ∂Bin(n, p), x ≤ n

Tactic:
binomial,

Goal state after:
Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : ↑I
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ ∀ᵐ (x : ℕ) ∂map ncard setBer(Iio n, p), x ≤ n
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n k : ℕ
p : ↑I
⊢ Bin(n, p).real {k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

Tactic:
binomial,

Goal state after:
n k : ℕ
p : ↑I
⊢ (map ncard setBer(Iio n, p)).real {k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ (∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x)).toReal = 1

Tactic:
← integral_eq_lintegral_of_nonneg_ae
    (ae_of_all _ fun x ↦ (cauchyPDF_pos x₀ hγ x).le) (by fun_prop),

Goal state after:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∫ (a : ℝ), cauchyPDFReal x₀ γ a = 1
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ((∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))) + 0).toReal = 1

Tactic:
add_zero,

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ (∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))).toReal = 1
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (gammaMeasure a r).real (Iic x) = (∫⁻ (x : ℝ) in Iic x, ENNReal.ofReal (gammaPDFReal a r x)).toReal

Tactic:
simp [gammaMeasure, gammaPDF, measureReal_def]

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ((∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))) + 0).toReal = 1

Tactic:
add_zero,

Goal state after:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ (∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))).toReal = 1
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
inst✝¹ : SFinite P
Y : Ω → 𝓨 × 𝓩
κ : Kernel 𝓧 (𝓨 × 𝓩)
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
⊢ HasCondDistrib (fun ω ↦ (Y ω).1) X κ.fst P

Tactic:
rw [Kernel.fst_eq]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
inst✝¹ : SFinite P
Y : Ω → 𝓨 × 𝓩
κ : Kernel 𝓧 (𝓨 × 𝓩)
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
⊢ HasCondDistrib (fun ω ↦ (Y ω).1) X (κ.map Prod.fst) P
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
⊢ Measure.map (fun ω x ↦ X x ω) μ = Measure.map (fun ω x ↦ Y x ω) ν

Tactic:
have : IsProbabilityMeasure μ := hX_ind.isProbabilityMeasure

Goal state after:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
this : IsProbabilityMeasure μ
⊢ Measure.map (fun ω x ↦ X x ω) μ = Measure.map (fun ω x ↦ Y x ω) ν
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ IsMarkovKernel (condExpKernel μ m)

Tactic:
rcases isEmpty_or_nonempty Ω with h | h

Goal state after:
case inl
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : IsEmpty Ω
⊢ IsMarkovKernel (condExpKernel μ m)

case inr
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : Nonempty Ω
⊢ IsMarkovKernel (condExpKernel μ m)
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map Function.diag μ

Tactic:
rcases isEmpty_or_nonempty Ω with h | h

Goal state after:
case inl
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : IsEmpty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map Function.diag μ

case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map Function.diag μ
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω ↦ ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]

Tactic:
rcases isEmpty_or_nonempty Ω with h | h

Goal state after:
case inl
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : IsEmpty Ω
⊢ (fun ω ↦ ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]

case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : Nonempty Ω
⊢ (fun ω ↦ ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f μ
⊢ μ[f | m ⊓ mΩ] =ᵐ[μ] fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
rcases isEmpty_or_nonempty Ω with h | h

Goal state after:
case inl
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f μ
h : IsEmpty Ω
⊢ μ[f | m ⊓ mΩ] =ᵐ[μ] fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

case inr
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f μ
h : Nonempty Ω
⊢ μ[f | m ⊓ mΩ] =ᵐ[μ] fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
ω : Ω
hω : f =ᵐ[(condExpKernel μ m) ω] AEStronglyMeasurable.mk f ⋯
⊢ ∫ (y : Ω), AEStronglyMeasurable.mk f ⋯ y ∂(condExpKernel μ m) ω = ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
integral_congr_ae hω

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
ω : Ω
hω : f =ᵐ[(condExpKernel μ m) ω] AEStronglyMeasurable.mk f ⋯
⊢ ∫ (y : Ω), AEStronglyMeasurable.mk f ⋯ y ∂(condExpKernel μ m) ω =
    ∫ (a : Ω), AEStronglyMeasurable.mk f ⋯ a ∂(condExpKernel μ m) ω
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 μ
⊢ ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun ω ↦ 1 | m] ω = 0 ∨ μ[t.indicator fun ω ↦ 1 | m] ω = 1

Tactic:
have (a : _) : IsFiniteMeasure (condExpKernel μ m a) := inferInstance
  have h := ae_of_ae_trim hm (Kernel.measure_eq_zero_or_one_of_indepSet_self h_indep)
  filter_upwards [condExpKernel_ae_eq_condExp hm ht, h] with ω hω_eq hω
  rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
have h'' := Measure.ae_ae_of_ae_comp h'
    filter_upwards [h.mgf_le, h''] with ω' h_mgf h' t
    rw [mgf_congr (Filter.EventuallyEq.symm h')]
    exact h_mgf t

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h2 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
a✝ : IsFiniteMeasure (κ ω')
t : ℝ
ht : 0 ≤ t
⊢ rexp (-t * ε) * mgf X (κ ω') t ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)

Tactic:
rw [exp_add]
    gcongr
    exact h1 t

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ stoppedProcess
      (fun i ↦
        ({a | ⊥ < hqX.localSeq n a} ∩ {a | ⊥ < hpX.localSeq n a}).indicator (stoppedProcess X (hpX.localSeq n) i))
      (hqX.localSeq n) i ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω

Tactic:
simp_rw [← Set.indicator_indicator]

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ stoppedProcess
      (fun i ↦
        {a | ⊥ < hqX.localSeq n a}.indicator
          ({a | ⊥ < hpX.localSeq n a}.indicator (stoppedProcess X (hpX.localSeq n) i)))
      (hqX.localSeq n) i ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Monotone fun N ↦ {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
intro m

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
m : ℕ
⊢ ∀ ⦃b : ℕ⦄, m ≤ b → (fun N ↦ {ω | X ω ∈ Set.Ioc ↑i ↑N}) m ⊆ (fun N ↦ {ω | X ω ∈ Set.Ioc ↑i ↑N}) b
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
f : X ⟶ Y
Z : Action (Type w) G
⊢ (μ Y Z).comp (rTensor (linearize k G Z) (linearizeMap f)) = (linearizeMap (f ▷ Z)).comp (μ X Z)

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
f : X ⟶ Y
Z : Action (Type w) G
⊢ (μ Z Y).comp (lTensor (linearize k G Z) (linearizeMap f)) = (linearizeMap (Z ◁ f)).comp (μ Z X)

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ↑(lid k (linearize k G X)) =
    ((linearizeMap (λ_ X).hom).comp (μ (𝟙_ (Action (Type w) G)) X)).comp (rTensor (linearize k G X) (ε k G))

Tactic:
by
  ext; simp

Goal state after: