mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case h
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha✝ : 0 ≤ a
ha : a = 0
⊢ 1 ≤ rexp (logRatio c)

Tactic:
simp only [Real.one_le_exp_iff]

Goal state after:
case h
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha✝ : 0 ≤ a
ha : a = 0
⊢ 0 ≤ logRatio c
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case neg.refine_1
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) ≤ 1

Tactic:
refine (ciInf_le h_bdd ⟨t + 1, lt_add_one t⟩).trans ?_

Goal state after:
case neg.refine_1
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (if ↑⟨t + 1, ⋯⟩ < 0 then 0 else 1) ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ stieltjesFunctionAux (fun p ↦ f p.2) ((), a) = stieltjesFunctionAux f a

Tactic:
by
  simp_rw [IsMeasurableRatCDF.stieltjesFunctionAux_def']

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 ρ
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) s

Tactic:
have : ∀ r, ∫⁻ x in s, preCDF ρ r x ∂ρ.fst = ∫⁻ x in s, (preCDF ρ r * 1) x ∂ρ.fst := by
    simp only [mul_one, forall_const]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) 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 κ ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)

Tactic:
filter_upwards [hf.nonneg a] with c hc

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
⊢ ∀ (q : ℚ), BddBelow (range fun r ↦ 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 κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
q : ℚ
⊢ 0 ∈ lowerBounds (range fun r ↦ f (a, c) ↑r)

Tactic:
simp [mem_lowerBounds, hc]

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 κ ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)

Tactic:
by
  filter_upwards [hf.nonneg a] with c hc
  refine fun q ↦ ⟨0, ?_⟩
  simp [mem_lowerBounds, hc]

Goal state after:
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ↑(cdf μ) x = (μ (Iic x)).toReal

Tactic:
← ofReal_cdf μ x,

Goal state after:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ↑(cdf μ) x = (ENNReal.ofReal (↑(cdf μ) x)).toReal
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:

Tactic:
∫ t in A, ⨅ r : Ioi q, f (a, t) r ∂(ν a)
      ≤ ⨅ r : Ioi q, (κ a).real (A ×ˢ Iic (r : ℝ)) := le_ciInf h
    _ = (κ a).real (A ×ˢ Iic (q : ℝ)) := by
        rw [measureReal_def, ← Measure.iInf_rat_gt_prod_Iic hA q]
        exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

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

Goal state before:
pp: case 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 ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ eLpNorm (fun x ↦ κ.densityProcess ν n a x s) 1 (ν a) < ∞

Tactic:
· exact (eLpNorm_densityProcess_le hκν n a s).trans_lt (measure_lt_top _ _)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
⊢ ((borelMarkovFromReal Ω η) a) s =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then (η a) (embeddingReal Ω '' s)
    else (embeddingReal Ω '' s).indicator 1 (Exists.choose ⋯)

Tactic:
have he := measurableEmbedding_embeddingReal Ω
  rw [borelMarkovFromReal_apply]
  split_ifs with h
  · rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs]
  · rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs, Measure.dirac_apply]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (X ω, Y ω)) P
h : cov[X, Y; P] = 0
L₁ L₂ : StrongDual ℝ ℝ
⊢ cov[⇑L₁ ∘ X, ⇑L₂ ∘ Y; P] = 0

Tactic:
by
    simp [Function.comp_def, ← toDual_symm_apply, covariance_mul_const_right,
      covariance_mul_const_left, h]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ charFunDual (Measure.map (Y - X) P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ (Y - X)) x ∂P) * I - ↑Var[⇑L ∘ (Y - X); P] / 2)

Tactic:
apply mul_left_cancel₀ (a := charFunDual (P.map X) L)

Goal state after:
case ha
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ charFunDual (Measure.map X P) L ≠ 0

case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ charFunDual (Measure.map X P) L * charFunDual (Measure.map (Y - X) P) L =
    charFunDual (Measure.map X P) L * cexp (↑(∫ (x : Ω), (⇑L ∘ (Y - X)) x ∂P) * I - ↑Var[⇑L ∘ (Y - X); P] / 2)
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 ν
a : α
s : Set β
hs : MeasurableSet s
⊢ Submartingale (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)

pp: case 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 : α
s : Set β
hs : MeasurableSet s
⊢ UniformIntegrable (fun n x ↦ κ.densityProcess ν n a x s) 1 (ν a)

Tactic:
· exact (martingale_densityProcess hκν a hs).submartingale

Goal state after:
case 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 : α
s : Set β
hs : MeasurableSet s
⊢ UniformIntegrable (fun n x ↦ κ.densityProcess ν n a x s) 1 (ν a)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (X i)
a b c : ι
i : ↥(Ioc a c)
h : ¬↑i ≤ b
⊢ Measurable fun c_1 ↦ IocProdIoc a b c c_1 i

Tactic:
simpa [IocProdIoc, h] using measurable_snd.eval

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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ (trajContent κ (frestrictLe a x₀)) (cylinder (Iic b) S) =
    lmarginalPartialTraj κ a b ((cylinder (Iic b) S).indicator 1) x₀

Tactic:
trajContent_cylinder mS,

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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ ((partialTraj κ a b) (frestrictLe a x₀)) S = lmarginalPartialTraj κ a b ((cylinder (Iic b) S).indicator 1) x₀
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 : α
⊢ (η a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
by
  suffices withDensity (κ + η) (fun a x ↦ Real.toNNReal
      (1 - rnDerivAux κ (κ + η) a x)) a {x | 1 ≤ rnDerivAux κ (κ + η) a x} = 0 by
    rwa [withDensity_one_sub_rnDerivAux κ η] at this
  simp_rw [ofNNReal_toNNReal]
  rw [Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]
  rotate_left
  · exact (measurableSet_singleton 0).preimage (by fun_prop)
  · fun_prop
  · fun_prop
  refine ae_of_all _ (fun x hx ↦ ?_)
  simp only [mem_ofPred_eq] at hx
  simp [hx]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ MeasurableSet (Set.univ.pi t)

Tactic:
· exact .univ_pi ht

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝ : Nonempty Θ
⊢ ↑C * κ.bound * P.bound * π Set.univ ≤ ↑C

Tactic:
rcases isEmpty_or_nonempty 𝓧

Goal state after:
case inr.inl
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝¹ : Nonempty Θ
h✝ : IsEmpty 𝓧
⊢ ↑C * κ.bound * P.bound * π Set.univ ≤ ↑C

case inr.inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝¹ : Nonempty Θ
h✝ : Nonempty 𝓧
⊢ ↑C * κ.bound * P.bound * π Set.univ ≤ ↑C
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ ↑C * (Kernel.const 𝓧 (Measure.dirac h𝓨.some)).bound * P.bound * π Set.univ ≤ ↑C * P.bound * π Set.univ

Tactic:
rcases isEmpty_or_nonempty 𝓧

Goal state after:
case inl
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝ : IsEmpty 𝓧
⊢ ↑C * (Kernel.const 𝓧 (Measure.dirac h𝓨.some)).bound * P.bound * π Set.univ ≤ ↑C * P.bound * π Set.univ

case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝ : Nonempty 𝓧
⊢ ↑C * (Kernel.const 𝓧 (Measure.dirac h𝓨.some)).bound * P.bound * π Set.univ ≤ ↑C * P.bound * π Set.univ
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: case hfg
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
x : 𝓧
⊢ ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ≤ ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂κ x

Tactic:
exact iInf_le_lintegral _

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
⊢ Ber(x, y, 0) = dirac y

Tactic:
by
  simp [bernoulliMeasure_def]

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
⊢ Ber(x, y, 1) = dirac x

Tactic:
by
  simp [bernoulliMeasure_def]

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

Goal state before:
pp: x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (y : ℝ) in Iio x, gammaPDF a r y = 0

Tactic:
rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]

Goal state after:
x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

x a r : ℝ
hx : x ≤ 0
⊢ EqOn (gammaPDF a r) (fun x ↦ 0) (Iio x)
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:
rw [binomial, map_ncard_setBernoulli_real_singleton (finite_Iio n), ncard_Iio_nat]

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
hf : Integrable f ((traj κ a) x₀)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i) in A, ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x ∂(partialTraj κ a b) x₀ =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' A, f y ∂(traj κ a) x₀

Tactic:
refine setIntegral_traj_partialTraj' hab ?_ hA
  rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf
  exact hf.comp_measurable measurable_snd

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

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
⊢ p.toOuterMeasure s = 0 ↔ Disjoint p.support s

Tactic:
rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero]
  exact funext_iff.symm.trans Set.indicator_eq_zero'

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

Goal state before:
pp: case refine_1
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ 0 ≤ᵐ[volume.restrict (Iic x)] gammaPDFReal a r

pp: case refine_2
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (gammaPDFReal a r) (volume.restrict (Iic x))

Tactic:
· exact ae_of_all _ fun b ↦ by simp [gammaPDFReal_nonneg ha hr]

Goal state after:
case refine_2
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (gammaPDFReal a r) (volume.restrict (Iic x))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (y : ℝ) in Iio x, paretoPDF t r y = 0

Tactic:
rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]

Goal state after:
t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

t r x : ℝ
hx : x ≤ t
⊢ EqOn (paretoPDF t r) (fun x ↦ 0) (Iio x)
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p✝ : ↑unitInterval
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun n ↦ ENNReal.ofReal (geometricPMFReal p n)) 1

Tactic:
apply ENNReal.hasSum_coe.mpr
    rw [← toNNReal_one]
    exact (geometricPMFRealSum hp_pos hp_le_one).toNNReal
      (fun n ↦ geometricPMFReal_nonneg hp_pos hp_le_one)

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

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ 0 ≤ 0

Tactic:
exact le_rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), p a * (f a) b else 0) = ∑' (a : α), p a * if b ∈ s then (f a) b else 0

Tactic:
by split_ifs <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
⊢ Measure.map f p.toMeasure = (map f p).toMeasure

Tactic:
ext s hs : 1; rw [PMF.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]

Goal state after:
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
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
nontriviality Ω

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
hf : StronglyMeasurable f
a✝ : Nontrivial Ω
⊢ StronglyMeasurable 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
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
nontriviality Ω

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
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (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
hf_int : Integrable f μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f ((condExpKernel μ m) ω)

Tactic:
nontriviality Ω

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f ((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
hf_int : Integrable f μ
⊢ Integrable (fun ω ↦ ∫ (y : Ω), ‖f y‖ ∂(condExpKernel μ m) ω) μ

Tactic:
nontriviality Ω

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (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
hf_int : Integrable f μ
⊢ Integrable (fun ω ↦ ‖∫ (y : Ω), f y ∂(condExpKernel μ m) ω‖) μ

Tactic:
nontriviality Ω

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
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (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
hf_int : Integrable f μ
⊢ Integrable (fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
nontriviality Ω

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
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ
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
⊢ Integrable (fun ω ↦ ((condExpKernel μ m) ω).real s) μ

Tactic:
nontriviality Ω

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ((condExpKernel μ m) ω).real s) μ
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ Indep (⨆ n ∈ t, s n) (limsup s f) κ μα

Tactic:
refine indep_of_indep_of_le_right (indep_biSup_compl h_le h_indep t) ?_

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ limsup s f ≤ ⨆ n ∈ tᶜ, s n