awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (t : ℝ) ↦
      t ^ (α - 1) * (1 - t) ^ (β - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)))

Tactic:
setIntegral_congr_fun measurableSet_Ioc fun x ⟨hx1, hx₂⟩ ↦ ?_

Premises used: HMul.hMul, HSub.hSub, Complex.ofReal, MeasureTheory.setIntegral_congr_fun, HPow.hPow, RCLike.re, measurableSet_Ioc, OfNat.ofNat, _private.0.ProbabilityTheory.lintegral_betaPDF_eq_one.match_7, Eq, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
refine :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioc 0 1) x →
      ∀ (hx1 : 0 < x) (hx₂ : x ≤ 1),
        x ^ (α - 1) * (1 - x) ^ (β - 1) =
          (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (t : ℝ) ↦
      t ^ (α - 1) * (1 - t) ^ (β - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioc fun x ⟨hx1, hx₂⟩ ↦ ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
norm_cast :
  x ^ (α - 1) * (1 - x) ^ (β - 1) =
    (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ (↑(α - 1) : ℂ) * (↑(1 - x) : ℂ) ^ (↑(β - 1) : ℂ))
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) =
    (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))

Tactic:
norm_cast
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
hx : 0 ≤ 1 - x
hx₁ : 0 ≤ x
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) =
    (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ (↑(α - 1) : ℂ) * (↑(1 - x) : ℂ) ^ (↑(β - 1) : ℂ))

Tactic:
rw [← Complex.ofReal_cpow, ← Complex.ofReal_cpow, RCLike.re_to_complex,
        Complex.re_mul_ofReal, Complex.ofReal_re]

Premises used: Complex.re_mul_ofReal, Complex.ofReal_cpow, Complex.ofReal_re, RCLike.re_to_complex
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
linarith : 1 - x < 0 → x - 1 + (1 - x - 0) = 0
⊢ 0 ≤ 1 - x

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
linarith : x < 0 → 0 - x + (x - 0) = 0
⊢ 0 ≤ x

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
a :
  @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
      (Measure.restrict volume (Ioc 0 1)) ↔
    IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)) volume 0 1
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1))

Tactic:
convert! betaIntegral_convergent (u := α) (v := β) (by simpa) (by simpa)

Premises used: Complex.betaIntegral_convergent
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ LE.le (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
a :
  @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
      (Measure.restrict volume (Ioc 0 1)) ↔
    IntegrableOn (ε := ℂ) (mα := Real.measurableSpace)
      (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)) (Ioc 0 1) volume
a₁ a₂ :
  @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
      (Measure.restrict volume (Ioc 0 1)) ↔
    @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
      (Measure.restrict volume (Ioc 0 1))
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
      (Measure.restrict volume (Ioc 0 1)) ↔
    IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)) volume 0 1

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by simp), IntegrableOn]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le, MeasureTheory.IntegrableOn
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

Tactic:
ae_restrict_of_forall_mem measurableSet_Ioo (fun x hx ↦ ?_)

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioo, Filter.EventuallyLE
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
hf :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x),
    LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

Tactic:
refine ae_restrict_of_forall_mem measurableSet_Ioo (fun x hx ↦ ?_)

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioo
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ 0 ≤ betaPDFReal α β x

Tactic:
betaPDFReal_pos hx.1 hx.2 hα hβ |>.le

Premises used: LT.lt.le, And.right, And.left, ProbabilityTheory.betaPDFReal_pos
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
h : (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x = betaPDFReal α β x
⊢ LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x)

Tactic:
convert! betaPDFReal_pos hx.1 hx.2 hα hβ |>.le using 1

Premises used: LT.lt.le, And.right, And.left, ProbabilityTheory.betaPDFReal_pos
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
h :
  (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x =
    if 0 < x ∧ x < 1 then 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0
h₁ h₂ :
  (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x = 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
⊢ (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x = betaPDFReal α β x

Tactic:
rw [betaPDFReal, if_pos ⟨hx.1, hx.2⟩]

Premises used: if_pos, ProbabilityTheory.betaPDFReal
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (Measure.restrict volume (Ioo 0 1))

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Eq (α := ℝ≥0∞) ((betaMeasure α β : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [betaMeasure, lintegral_betaPDF_eq_one hα hβ]

Premises used: ProbabilityTheory.lintegral_betaPDF_eq_one, ProbabilityTheory.betaMeasure
-- Module: Mathlib.Probability.Distributions.Binomial
Goal:
R : Type u_1
Ω : Type u_2
inst : MeasurableSpace R
inst_1 : AddMonoidWithOne R
m : MeasurableSpace Ω
P : Measure Ω
X : Ω → R
n : ℕ
p : (↑I : Type)
⊢ AEMeasurable Set.ncard setBer(Set.Iio n, p)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Binomial
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : (↑I : Type)
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ Measurable (β := Prop) fun (x : ℕ) ↦ x ≤ n

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Binomial
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : (↑I : Type)
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ AEMeasurable Set.ncard setBer(Set.Iio n, p)

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

Tactic:
rw [hX.ae_iff (p := (· ≤ n)) <| by fun_prop, binomial,
    ae_map_iff (by fun_prop) (Set.finite_Iic _).measurableSet]

Premises used: ProbabilityTheory.binomial, Set.finite_Iic, ProbabilityTheory.HasLaw.ae_iff, MeasureTheory.ae_map_iff, Set.Finite.measurableSet
-- Module: Mathlib.Probability.Distributions.Binomial
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : (↑I : Type)
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
h : ∀ (s : Set ℕ) (hs : s ⊆ Set.Iio n), s.ncard ≤ n
⊢ ∀ᵐ (x : Set ℕ) ∂setBer(Set.Iio n, p), x.ncard ≤ n

Tactic:
filter_upwards [setBernoulli_ae_subset] with s hs

Premises used: ProbabilityTheory.setBernoulli_ae_subset
-- Module: Mathlib.Probability.Distributions.Binomial
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : (↑I : Type)
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
s : Set ℕ
hs : s ⊆ Set.Iio n
⊢ s.ncard ≤ n

Tactic:
simpa using Set.ncard_le_ncard hs

Premises used: Set.ncard_le_ncard
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
h : ∀ (x : ℝ), cauchyPDFReal x₀ 0 x = 0 x
⊢ cauchyPDFReal x₀ 0 = 0

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ x : ℝ
⊢ cauchyPDFReal x₀ 0 x = 0 x

Tactic:
simp [cauchyPDFReal]

Premises used: ProbabilityTheory.cauchyPDFReal
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
x : ℝ
⊢ cauchyPDFReal x₀ γ x = π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹

Tactic:
rfl
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
x : ℝ
pos :
  ∀ (h : γ = 0),
    π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
      π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹
neg :
  ∀ (h : ¬γ = 0),
    π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
      π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹
⊢ π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
    π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹

Tactic:
by_cases h : γ = 0
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
x : ℝ
h : γ = 0
⊢ π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
    π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹

Tactic:
simp [h]
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
x : ℝ
h : ¬γ = 0
⊢ π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
    π⁻¹ * (↑γ : ℝ)⁻¹ * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹

Tactic:
field
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
h : ∀ (x : ℝ), cauchyPDF x₀ 0 x = 0 x
⊢ cauchyPDF x₀ 0 = 0

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ x : ℝ
⊢ cauchyPDF x₀ 0 x = 0 x

Tactic:
simp [cauchyPDF]

Premises used: ProbabilityTheory.cauchyPDF
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
x : ℝ
⊢ cauchyPDF x₀ γ x = ENNReal.ofReal (cauchyPDFReal x₀ γ x)

Tactic:
rfl
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
⊢ StronglyMeasurable (cauchyPDFReal x₀ γ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
⊢ Measurable (β := ℝ≥0∞) fun (x : ℝ) ↦ ENNReal.ofReal (cauchyPDFReal x₀ γ x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
⊢ StronglyMeasurable (cauchyPDF x₀ γ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
x : ℝ
⊢ 0 < π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
simp : π⁻¹ * (↑γ : ℝ)⁻¹ * ((↑γ : ℝ) * π) = 1
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cauchyPDFReal x₀ γ x) 1

Tactic:
simp [cauchyPDFReal_def', NNReal.coe_inv, integral_const_mul,
    integral_sub_right_eq_self (f := fun x : ℝ ↦ (1 + (x / ↑γ) ^ 2)⁻¹),
    integral_comp_div (g := fun x : ℝ ↦ (1 + x ^ 2)⁻¹)]

Premises used: MeasureTheory.integral_const_mul, HDiv.hDiv, NNReal.coe_inv, ProbabilityTheory.cauchyPDFReal_def', Inv.inv, HPow.hPow, HAdd.hAdd, OfNat.ofNat, MeasureTheory.integral_sub_right_eq_self, MeasureTheory.Measure.integral_comp_div
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ π⁻¹ * (↑γ : ℝ)⁻¹ * ((↑γ : ℝ) * π) = 1

Tactic:
field
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
pos : ∀ (h : γ = 0), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
neg : ∀ (h : γ ≠ 0), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume

Tactic:
by_cases! h : γ = 0
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
pos : @Integrable ℝ _ _ ℝ MeasureSpace.toMeasurableSpace 0 volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume

Tactic:
simp only [h, cauchyPDFReal_scale_zero]

Premises used: ProbabilityTheory.cauchyPDFReal_scale_zero
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ @Integrable ℝ _ _ ℝ MeasureSpace.toMeasurableSpace 0 volume

Tactic:
integrable_zero _ _ _

Premises used: MeasureTheory.integrable_zero
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ @Integrable ℝ _ _ ℝ MeasureSpace.toMeasurableSpace 0 volume

Tactic:
exact integrable_zero _ _ _

Premises used: MeasureTheory.integrable_zero
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
h : γ ≠ 0
neg : Ne (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦ cauchyPDFReal x₀ γ a) 0
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume

Tactic:
apply Integrable.of_integral_ne_zero

Premises used: MeasureTheory.Integrable.of_integral_ne_zero
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
h : γ ≠ 0
⊢ Ne (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦ cauchyPDFReal x₀ γ a) 0

Tactic:
simp [h, integral_cauchyPDFReal_eq_one]

Premises used: ProbabilityTheory.integral_cauchyPDFReal_eq_one
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (cauchyPDFReal x₀ γ) volume

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
rw : (∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x)).toReal = 1
rw₁ : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦ cauchyPDFReal x₀ γ a) 1
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x) = 1

Tactic:
rw [← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae
    (ae_of_all _ fun x ↦ (cauchyPDF_pos x₀ hγ x).le) (by fun_prop),
    integral_cauchyPDFReal_eq_one x₀ hγ]

Premises used: ProbabilityTheory.integral_cauchyPDFReal_eq_one, LT.lt.le, ProbabilityTheory.cauchyPDF_pos, MeasureTheory.ae_of_all, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ cauchyMeasure x₀ γ = withDensity volume (cauchyPDF x₀ γ)

Tactic:
if_neg hγ

Premises used: if_neg, ProbabilityTheory.cauchyMeasure
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
⊢ cauchyMeasure x₀ 0 = dirac x₀

Tactic:
if_pos rfl

Premises used: if_pos, ProbabilityTheory.cauchyMeasure, rfl
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
pos : ∀ (h : γ = 0), Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
neg : ∀ (h : ¬γ = 0), Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
by_cases h : γ = 0
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [cauchyMeasure_of_scale_ne_zero, h]

Premises used: ProbabilityTheory.cauchyMeasure_of_scale_ne_zero
-- Module: Mathlib.Probability.Distributions.Cauchy
Goal:
x₀ : ℝ
γ : ℝ≥0
h : ¬γ = 0
⊢ Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [cauchyMeasure_of_scale_ne_zero, h]

Premises used: ProbabilityTheory.cauchyMeasure_of_scale_ne_zero
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r x : ℝ
⊢ ENNReal.ofReal
      (if 0 ≤ x then HPow.hPow (β := ℝ) r 1 / Gamma 1 * x ^ HSub.hSub (α := ℝ) 1 1 * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)

Tactic:
simp only [rpow_one, Gamma_one, div_one, sub_self, rpow_zero, mul_one]

Premises used: sub_self, Real.Gamma_one, Real.rpow_zero, Real.rpow_one, mul_one, div_one
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r x : ℝ
hx : x < 0
⊢ exponentialPDF r x = 0

Tactic:
gammaPDF_of_neg hx

Premises used: ProbabilityTheory.gammaPDF, ProbabilityTheory.exponentialPDF, ProbabilityTheory.gammaPDF_of_neg, ProbabilityTheory.exponentialPDFReal
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r x : ℝ
hx : 0 ≤ x
⊢ exponentialPDF r x = ENNReal.ofReal (r * rexp (-(r * x)))

Tactic:
simp only [exponentialPDF_eq, if_pos hx]

Premises used: ProbabilityTheory.exponentialPDF_eq, if_pos
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
x r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (y : ℝ) in Iio x, exponentialPDF r y = 0

Tactic:
lintegral_gammaPDF_of_nonpos hx

Premises used: ProbabilityTheory.lintegral_gammaPDF_of_nonpos, ProbabilityTheory.gammaPDF, ProbabilityTheory.exponentialPDF, ProbabilityTheory.exponentialPDFReal
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
⊢ Measurable (exponentialPDFReal r)

Tactic:
measurable_gammaPDFReal 1 r

Premises used: ProbabilityTheory.measurable_gammaPDFReal, ProbabilityTheory.exponentialPDFReal, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
⊢ StronglyMeasurable (exponentialPDFReal r)

Tactic:
stronglyMeasurable_gammaPDFReal 1 r

Premises used: ProbabilityTheory.stronglyMeasurable_gammaPDFReal, ProbabilityTheory.exponentialPDFReal, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
x r : ℝ
hr : 0 < r
hx : 0 < x
⊢ 0 < exponentialPDFReal r x

Tactic:
gammaPDFReal_pos zero_lt_one hr hx

Premises used: zero_lt_one, ProbabilityTheory.gammaPDFReal_pos, ProbabilityTheory.exponentialPDFReal
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
⊢ 0 ≤ exponentialPDFReal r x

Tactic:
gammaPDFReal_nonneg zero_lt_one hr x

Premises used: ProbabilityTheory.gammaPDFReal_nonneg, zero_lt_one, ProbabilityTheory.exponentialPDFReal
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
⊢ ∫⁻ (x : ℝ), exponentialPDF r x = 1

Tactic:
lintegral_gammaPDF_eq_one zero_lt_one hr

Premises used: ProbabilityTheory.gammaPDF, ProbabilityTheory.exponentialPDF, zero_lt_one, ProbabilityTheory.exponentialPDFReal, ProbabilityTheory.lintegral_gammaPDF_eq_one
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
⊢ IsProbabilityMeasure (expMeasure r)

Tactic:
isProbabilityMeasure_gammaMeasure zero_lt_one hr

Premises used: ProbabilityTheory.isProbabilityMeasure_gammaMeasure, ProbabilityTheory.expMeasure, zero_lt_one
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
⊢ (↑(cdf (expMeasure r)) : ℝ → ℝ) x =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦
      exponentialPDFReal r x

Tactic:
cdf_gammaMeasure_eq_integral zero_lt_one hr x

Premises used: ProbabilityTheory.expMeasure, zero_lt_one, ProbabilityTheory.exponentialPDFReal, ProbabilityTheory.cdf_gammaMeasure_eq_integral
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
⊢ (↑(cdf (expMeasure r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, exponentialPDF r x).toReal

Tactic:
cdf_gammaMeasure_eq_lintegral zero_lt_one hr x

Premises used: ProbabilityTheory.gammaPDF, ProbabilityTheory.exponentialPDF, ProbabilityTheory.expMeasure, ProbabilityTheory.cdf_gammaMeasure_eq_lintegral, zero_lt_one, ProbabilityTheory.exponentialPDFReal
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ -1 * rexp (-r * id y)) (-1 * (rexp (-r * id x) * (-r * 1))) x

Tactic:
(((hasDerivAt_id x).const_mul (-r)).exp.const_mul (-1))

Premises used: HasDerivAt.exp, hasDerivAt_id, HasDerivAt.const_mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r x : ℝ
h : Eq (α := ℝ → ℝ) (fun (a : ℝ) ↦ -rexp (-(r * a))) fun (y : ℝ) ↦ -1 * rexp (-r * id y)
h₁ : r * rexp (-(r * x)) = -1 * (rexp (-r * id x) * (-r * 1))
⊢ HasDerivAt (fun (a : ℝ) ↦ -rexp (-(r * a))) (r * rexp (-(r * x))) x

Tactic:
convert! (((hasDerivAt_id x).const_mul (-r)).exp.const_mul (-1)) using 1

Premises used: HasDerivAt.exp, hasDerivAt_id, HasDerivAt.const_mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r x : ℝ
⊢ Eq (α := ℝ → ℝ) (fun (a : ℝ) ↦ -rexp (-(r * a))) fun (y : ℝ) ↦ -1 * rexp (-r * id y)

Tactic:
simp only [one_mul, id_eq, neg_mul]

Premises used: neg_mul, one_mul, id_eq
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r x : ℝ
⊢ r * rexp (-(r * x)) = -1 * (rexp (-r * id x) * (-r * 1))

Tactic:
simp only [id_eq, neg_mul, mul_one, mul_neg, one_mul, neg_neg, mul_comm]

Premises used: neg_neg, mul_comm, neg_mul, mul_one, one_mul, mul_neg, id_eq
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
b x : ℝ
hb : 0 < b
simp : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * x)) (Ioc 0 x) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-(b * x))) (Ioc 0 x) volume

Tactic:
simp only [neg_mul_eq_neg_mul]

Premises used: neg_mul_eq_neg_mul
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
b x : ℝ
hb : 0 < b
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * x)) (Ioc 0 x) volume

Tactic:
(exp_neg_integrableOn_Ioi _ hb).mono_set Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set, exp_neg_integrableOn_Ioi
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
b x : ℝ
hb : 0 < b
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * x)) (Ioc 0 x) volume

Tactic:
exact (exp_neg_integrableOn_Ioi _ hb).mono_set Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set, exp_neg_integrableOn_Ioi