awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
rw : HaveLebesgueDecomposition (map X ℙ ∗ₘ map Y ℙ) μ ∧ map X ℙ ∗ₘ map Y ℙ ≪ μ
⊢ HasPDF (X * Y) ℙ μ

Tactic:
rw [hasPDF_iff_of_aemeasurable (by fun_prop),
    hXY.map_mul_eq_map_mconv_map₀' (by fun_prop) (by fun_prop) σX σY]

Premises used: ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀', MeasureTheory.hasPDF_iff_of_aemeasurable
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ HaveLebesgueDecomposition (map X ℙ ∗ₘ map Y ℙ) μ ∧ map X ℙ ∗ₘ map Y ℙ ≪ μ

Tactic:
⟨?_, mconv_absolutelyContinuous HasPDF.absolutelyContinuous⟩

Premises used: MeasureTheory.Measure.mconv_absolutelyContinuous, And.intro, MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
refine : HaveLebesgueDecomposition (map X ℙ ∗ₘ map Y ℙ) μ
⊢ HaveLebesgueDecomposition (map X ℙ ∗ₘ map Y ℙ) μ ∧ map X ℙ ∗ₘ map Y ℙ ≪ μ

Tactic:
refine ⟨?_, mconv_absolutelyContinuous HasPDF.absolutelyContinuous⟩
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
hν₁ : map X ℙ ≪ μ
hν₂ : map Y ℙ ≪ μ
⊢ HaveLebesgueDecomposition (map X ℙ ∗ₘ map Y ℙ) μ

Tactic:
apply HaveLebesgueDecomposition.mconv

Premises used: MeasureTheory.HaveLebesgueDecomposition.mconv
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ map X ℙ ≪ μ

Tactic:
HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ map X ℙ ≪ μ

Tactic:
exact HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ map Y ℙ ≪ μ

Tactic:
HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this_1 : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ map Y ℙ ≪ μ

Tactic:
exact HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
⊢ HasPDF (X * Y) ℙ μ

Tactic:
apply hXY.mul_hasPDF'

Premises used: ProbabilityTheory.IndepFun.mul_hasPDF'
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ SigmaFinite (m0 := mG) (map X ℙ)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Premises used: MeasureTheory.IsFiniteMeasure.toSigmaFinite
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ SigmaFinite (m0 := mG) (map Y ℙ)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Premises used: MeasureTheory.IsFiniteMeasure.toSigmaFinite
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SigmaFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
rw : rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
⊢ pdf (X * Y) ℙ μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
rw [pdf, hXY.map_mul_eq_map_mconv_map₀' (HasPDF.aemeasurable' μ) (HasPDF.aemeasurable' μ) σX σY]

Premises used: MeasureTheory.HasPDF.aemeasurable', MeasureTheory.pdf, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀'
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SigmaFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
hν₁ : map X ℙ ≪ μ
hν₂ : map Y ℙ ≪ μ
⊢ rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
apply rnDeriv_mconv'

Premises used: MeasureTheory.rnDeriv_mconv'
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SigmaFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
⊢ map X ℙ ≪ μ

Tactic:
HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SigmaFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
⊢ map X ℙ ≪ μ

Tactic:
exact HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SigmaFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
⊢ map Y ℙ ≪ μ

Tactic:
HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SigmaFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
σX : SigmaFinite (m0 := mG) (map X ℙ)
σY : SigmaFinite (m0 := mG) (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
⊢ map Y ℙ ≪ μ

Tactic:
exact HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
rw : rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
⊢ pdf (X * Y) ℙ μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
rw [pdf, hXY.map_mul_eq_map_mconv_map₀ (HasPDF.aemeasurable' μ) (HasPDF.aemeasurable' μ)]

Premises used: ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀, MeasureTheory.HasPDF.aemeasurable', MeasureTheory.pdf
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
hν₁ : map X ℙ ≪ μ
hν₂ : map Y ℙ ≪ μ
⊢ rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
apply rnDeriv_mconv

Premises used: MeasureTheory.rnDeriv_mconv
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ map X ℙ ≪ μ

Tactic:
HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ map X ℙ ≪ μ

Tactic:
exact HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ map Y ℙ ≪ μ

Tactic:
HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
X Y : Ω → G
inst_4 : SFinite μ
inst_5 : HasPDF X ℙ μ
inst_6 : HasPDF Y ℙ μ
inst_7 : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ map Y ℙ ≪ μ

Tactic:
exact HasPDF.absolutelyContinuous

Premises used: MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 < beta α β

Tactic:
div_pos (mul_pos (Real.Gamma_pos_of_pos hα) (Real.Gamma_pos_of_pos hβ))
    (Real.Gamma_pos_of_pos (add_pos hα hβ))

Premises used: Real.Gamma_pos_of_pos, add_pos, mul_pos, ProbabilityTheory.beta, div_pos
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
rw : beta α β = (Gamma (↑α : ℂ) * Gamma (↑β : ℂ) / Gamma ((↑α : ℂ) + (↑β : ℂ))).re
hu : 0 < (↑α : ℂ).re
hv : 0 < (↑β : ℂ).re
⊢ beta α β = ((↑α : ℂ).betaIntegral (↑β : ℂ)).re

Tactic:
rw [betaIntegral_eq_Gamma_mul_div]

Premises used: Complex.betaIntegral_eq_Gamma_mul_div
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
simp_rw :
  Real.Gamma α * Real.Gamma β / Real.Gamma (α + β) =
    ((↑(Real.Gamma α) : ℂ) * (↑(Real.Gamma β) : ℂ) / (↑(Real.Gamma (α + β)) : ℂ)).re
⊢ beta α β = (Gamma (↑α : ℂ) * Gamma (↑β : ℂ) / Gamma ((↑α : ℂ) + (↑β : ℂ))).re

Tactic:
simp_rw [beta, ← ofReal_add α β, Gamma_ofReal]

Premises used: Complex.ofReal_add, ProbabilityTheory.beta, Complex.Gamma_ofReal
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Real.Gamma α * Real.Gamma β / Real.Gamma (α + β) = Real.Gamma α * Real.Gamma β / Real.Gamma (α + β)
⊢ Real.Gamma α * Real.Gamma β / Real.Gamma (α + β) =
    ((↑(Real.Gamma α) : ℂ) * (↑(Real.Gamma β) : ℂ) / (↑(Real.Gamma (α + β)) : ℂ)).re

Tactic:
norm_cast
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 < (↑α : ℂ).re

Tactic:
simpa
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 < (↑β : ℂ).re

Tactic:
simpa
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β x : ℝ
⊢ betaPDF α β x = ENNReal.ofReal (if 0 < x ∧ x < 1 then 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0)

Tactic:
rfl

Premises used: ProbabilityTheory.betaPDF, rfl, ProbabilityTheory.betaPDFReal
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β x : ℝ
hx : x ≤ 0
⊢ betaPDF α β x = 0

Tactic:
simp [betaPDF_eq, hx.not_gt]

Premises used: ProbabilityTheory.betaPDF_eq, LE.le.not_gt
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β x : ℝ
hx : 1 ≤ x
⊢ betaPDF α β x = 0

Tactic:
simp [betaPDF_eq, hx.not_gt]

Premises used: ProbabilityTheory.betaPDF_eq, LE.le.not_gt
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β x : ℝ
hx_pos : 0 < x
hx_lt : x < 1
rw :
  ENNReal.ofReal (if 0 < x ∧ x < 1 then 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0) =
    ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ rw₂ :
  ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) =
    ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ betaPDF α β x = ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

Tactic:
rw [betaPDF_eq, if_pos ⟨hx_pos, hx_lt⟩]

Premises used: ProbabilityTheory.betaPDF_eq, if_pos
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₄ :
  ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₅ :
  ∫⁻ (x : ℝ) in Ici 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) +
      ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₆ : ℝ
rw₇ :
  0 + ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₈ :
  ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₉ :
  ∫⁻ (x : ℝ) in Iio 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁₀ :
  ∫⁻ (x : ℝ) in Iio 1 ∩ Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁₁ :
  ∫⁻ (x : ℝ) in Ioo 0 1, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁₂ rw₁₃ :
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) ∂volume =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

Tactic:
rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]

Premises used: ProbabilityTheory.betaPDF_eq_zero_of_nonpos, HMul.hMul, ProbabilityTheory.betaPDF, ENNReal.ofReal, measurableSet_Iio, HSub.hSub, _private.0.ProbabilityTheory.lintegral_betaPDF.match_1, ProbabilityTheory.betaPDF_of_pos_lt_one, MeasureTheory.setLIntegral_congr_fun, HDiv.hDiv, measurableSet_Iic, MeasureTheory.Measure.restrict_restrict, MeasureTheory.lintegral_add_compl, zero_add, Set.Iio_inter_Ioi, Set.compl_Iic, HPow.hPow, measurableSet_Ioo, ProbabilityTheory.beta, ProbabilityTheory.betaPDF_eq_zero_of_one_le, Set.compl_Ici, MeasureTheory.setLIntegral_eq_zero, OfNat.ofNat, measurableSet_Ici, Eq
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
rw : 0 < 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
⊢ 0 < betaPDFReal α β x

Tactic:
rw [betaPDFReal, if_pos ⟨hx1, hx2⟩]

Premises used: if_pos, ProbabilityTheory.betaPDFReal
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
linarith : 1 - x ≤ 0 → x - 1 + (1 - x - 0) = 0
⊢ 0 < 1 - x

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
⊢ 0 < 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

Tactic:
exact mul_pos (mul_pos (one_div_pos.2 (beta_pos hα hβ)) (Real.rpow_pos_of_pos hx1 (α - 1)))
    (Real.rpow_pos_of_pos (by linarith) (β - 1))

Premises used: Iff.mpr, Real.rpow_pos_of_pos, HSub.hSub, mul_pos, one_div_pos, ProbabilityTheory.beta_pos, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
⊢ StronglyMeasurable (betaPDFReal α β)

Tactic:
(measurable_betaPDFReal α β).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, ProbabilityTheory.measurable_betaPDFReal
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
      1 / beta α β * a ^ (α - 1) * (1 - a) ^ (β - 1))
    1
hf :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (Measure.restrict volume (Ioo 0 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = 1

Tactic:
rw [lintegral_betaPDF, ← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae, ProbabilityTheory.lintegral_betaPDF, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
simp_rw :
  (1 / beta α β *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
        a ^ (α - 1) * (1 - a) ^ (β - 1)) =
    1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
      1 / beta α β * a ^ (α - 1) * (1 - a) ^ (β - 1))
    1

Tactic:
simp_rw [mul_assoc, integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, mul_assoc
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
field_simp :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
        a ^ (α - 1) * (1 - a) ^ (β - 1)) /
      beta α β =
    1
⊢ (1 / beta α β *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
        a ^ (α - 1) * (1 - a) ^ (β - 1)) =
    1

Tactic:
field_simp
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ LE.le (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.Probability.Distributions.Beta
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
rw :
  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)))
rw₁ :
  @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
        a ^ (α - 1) * (1 - a) ^ (β - 1)) /
      beta α β =
    1

Tactic:
rw [div_eq_one_iff_eq (ne_of_gt (beta_pos hα hβ)), beta_eq_betaIntegralReal α β hα hβ,
      betaIntegral, intervalIntegral.integral_of_le (by norm_num),
      ← integral_Ioc_eq_integral_Ioo, ← RCLike.re_to_complex, ← integral_re]

Premises used: div_eq_one_iff_eq, ne_of_gt, ProbabilityTheory.beta_eq_betaIntegralReal, MeasureTheory.integral_Ioc_eq_integral_Ioo, intervalIntegral.integral_of_le, Complex.betaIntegral, ProbabilityTheory.beta_pos, integral_re, RCLike.re_to_complex