awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
⊢ ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x

Tactic:
exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
⊢ IsEmpty (Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel)

Tactic:
have : IsEmpty (Subtype (@IsMarkovKernel 𝓧 𝓨 m𝓧 m𝓨)) := by
    simp only [isEmpty_subtype]
    exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : Nonempty 𝓧
inst_1 : IsEmpty 𝓨
this : IsEmpty (Subtype (α := Kernel 𝓧 𝓨) IsMarkovKernel)
⊢ minimaxRisk ℓ P = ∞

Tactic:
simp [minimaxRisk, iInf_subtype']

Premises used: ProbabilityTheory.minimaxRisk, iInf_subtype'
-- Module: Mathlib.Probability.Decision.Risk.Defs
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : Nonempty 𝓨
inst_1 : IsEmpty Θ
⊢ minimaxRisk ℓ P = 0

Tactic:
simp [minimaxRisk, iInf_subtype']

Premises used: ProbabilityTheory.minimaxRisk, iInf_subtype'
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
⊢ HasPDF X ℙ μ ↔ AEMeasurable X ℙ ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ

Tactic:
⟨fun ⟨h₁, h₂, h₃⟩ ↦ ⟨h₁, h₂, h₃⟩, fun ⟨h₁, h₂, h₃⟩ ↦ ⟨h₁, h₂, h₃⟩⟩

Premises used: AEMeasurable, MeasureTheory.HasPDF.mk, MeasureTheory.Measure.AbsolutelyContinuous, MeasureTheory.HasPDF, MeasureTheory.Measure.HaveLebesgueDecomposition, And, _private.0.MeasureTheory.hasPDF_iff.match_2, MeasureTheory.Measure.map, And.intro, Iff.intro, _private.0.MeasureTheory.hasPDF_iff.match_1
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
rw :
  AEMeasurable X ℙ ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ ↔
    HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
⊢ HasPDF X ℙ μ ↔ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ

Tactic:
rw [hasPDF_iff]

Premises used: MeasureTheory.hasPDF_iff
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
⊢ AEMeasurable X ℙ ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ ↔
    HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ

Tactic:
simp only [hX, true_and]

Premises used: true_and
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
inst_1 : HasPDF X ℙ μ
⊢ AEMeasurable X ℙ

Tactic:
HasPDF.aemeasurable' μ

Premises used: MeasureTheory.HasPDF.aemeasurable'
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X Y : Ω → E
ℙ : Measure Ω
μ : Measure E
inst_1 : HasPDF X ℙ μ
⊢ HaveLebesgueDecomposition (map X ℙ) μ

Tactic:
HasPDF.haveLebesgueDecomposition'

Premises used: MeasureTheory.HasPDF.haveLebesgueDecomposition'
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
inst_1 : HasPDF X ℙ μ
⊢ map X ℙ ≪ μ

Tactic:
HasPDF.absolutelyContinuous'

Premises used: MeasureTheory.HasPDF.absolutelyContinuous'
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
inst_1 : HasPDF X ℙ μ
h : Measurable X
⊢ QuasiMeasurePreserving X ℙ μ

Tactic:
{ measurable := h
    absolutelyContinuous := HasPDF.absolutelyContinuous .. }

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X Y : Ω → E
ℙ : Measure Ω
μ : Measure E
hXY : X =ᶠ[ae ℙ] Y
hX : HasPDF X ℙ μ
⊢ HasPDF Y ℙ μ

Tactic:
⟨(HasPDF.aemeasurable X ℙ μ).congr hXY, ℙ.map_congr hXY ▸ hX.haveLebesgueDecomposition,
    ℙ.map_congr hXY ▸ hX.absolutelyContinuous⟩

Premises used: AEMeasurable.congr, MeasureTheory.HasPDF.mk, Eq.rec, MeasureTheory.HasPDF.haveLebesgueDecomposition, MeasureTheory.Measure.map_congr, MeasureTheory.HasPDF.aemeasurable, MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X Y : Ω → E
ℙ : Measure Ω
μ : Measure E
hXY : X =ᶠ[ae ℙ] Y
⊢ HasPDF X ℙ μ ↔ HasPDF Y ℙ μ

Tactic:
⟨fun _ ↦ HasPDF.congr hXY, fun _ ↦ HasPDF.congr hXY.symm⟩

Premises used: MeasureTheory.HasPDF.congr, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ HasPDF X ℙ μ

Tactic:
⟨hX, ?_, ?_⟩

Premises used: MeasureTheory.HasPDF.mk
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
refine_1 : HaveLebesgueDecomposition (map X ℙ) μ
refine_2 : map X ℙ ≪ μ
⊢ HasPDF X ℙ μ

Tactic:
refine ⟨hX, ?_, ?_⟩
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
refine_1 : (μ.withDensity f).HaveLebesgueDecomposition μ
⊢ HaveLebesgueDecomposition (map X ℙ) μ

Tactic:
rw [h]
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
refine_2 : μ.withDensity f ≪ μ
⊢ map X ℙ ≪ μ

Tactic:
rw [h]
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
refine_1 : (μ.withDensity (AEMeasurable.mk f hf)).HaveLebesgueDecomposition μ
⊢ (μ.withDensity f).HaveLebesgueDecomposition μ

Tactic:
rw [withDensity_congr_ae hf.ae_eq_mk]

Premises used: MeasureTheory.withDensity_congr_ae, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity (AEMeasurable.mk f hf)).HaveLebesgueDecomposition μ

Tactic:
haveLebesgueDecomposition_withDensity μ hf.measurable_mk

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_withDensity, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity (AEMeasurable.mk f hf)).HaveLebesgueDecomposition μ

Tactic:
exact haveLebesgueDecomposition_withDensity μ hf.measurable_mk

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_withDensity, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ μ.withDensity f ≪ μ

Tactic:
withDensity_absolutelyContinuous μ f

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ μ.withDensity f ≪ μ

Tactic:
exact withDensity_absolutelyContinuous μ f

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
⊢ pdf X ℙ μ = rnDeriv (map X ℙ) μ

Tactic:
rfl

Premises used: MeasureTheory.pdf, rfl
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
rw : rnDeriv 0 μ =ᶠ[ae μ] 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
rw [pdf_def, map_of_not_aemeasurable hX]

Premises used: MeasureTheory.pdf_def, MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ rnDeriv 0 μ =ᶠ[ae μ] 0

Tactic:
rnDeriv_zero μ

Premises used: MeasureTheory.Measure.rnDeriv_zero
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ rnDeriv 0 μ =ᶠ[ae μ] 0

Tactic:
exact rnDeriv_zero μ

Premises used: MeasureTheory.Measure.rnDeriv_zero
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬HaveLebesgueDecomposition (map X ℙ) μ
⊢ pdf X ℙ μ = 0

Tactic:
rnDeriv_of_not_haveLebesgueDecomposition h

Premises used: MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition, MeasureTheory.pdf
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬pdf X ℙ μ =ᶠ[ae μ] 0
contrapose : ∀ (h : ¬AEMeasurable X ℙ), pdf X ℙ μ =ᶠ[ae μ] 0
⊢ AEMeasurable X ℙ

Tactic:
contrapose h
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬AEMeasurable X ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
pdf_of_not_aemeasurable h

Premises used: MeasureTheory.pdf_of_not_aemeasurable
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬AEMeasurable X ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
exact pdf_of_not_aemeasurable h

Premises used: MeasureTheory.pdf_of_not_aemeasurable
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ HasPDF X ℙ μ

Tactic:
⟨?_, ?_, hac⟩

Premises used: MeasureTheory.HasPDF.mk
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
refine_1 : AEMeasurable X ℙ
refine_2 : HaveLebesgueDecomposition (map X ℙ) μ
⊢ HasPDF X ℙ μ

Tactic:
refine ⟨?_, ?_, hac⟩
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ AEMeasurable X ℙ

Tactic:
aemeasurable_of_pdf_ne_zero X hpdf

Premises used: MeasureTheory.aemeasurable_of_pdf_ne_zero
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ AEMeasurable X ℙ

Tactic:
exact aemeasurable_of_pdf_ne_zero X hpdf

Premises used: MeasureTheory.aemeasurable_of_pdf_ne_zero
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬pdf X ℙ μ =ᶠ[ae μ] 0
refine_2 : ∀ (hpdf : ¬HaveLebesgueDecomposition (map X ℙ) μ), pdf X ℙ μ =ᶠ[ae μ] 0
⊢ HaveLebesgueDecomposition (map X ℙ) μ

Tactic:
contrapose hpdf
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬HaveLebesgueDecomposition (map X ℙ) μ
⊢ pdf X ℙ μ = 0

Tactic:
have := pdf_of_not_haveLebesgueDecomposition hpdf
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬HaveLebesgueDecomposition (map X ℙ) μ
this : pdf X ℙ μ = 0
⊢ ∀ (a : E), pdf X ℙ μ a = 0 a

Tactic:
congrFun this

Premises used: congrFun
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hac : map X ℙ ≪ μ
hpdf : ¬HaveLebesgueDecomposition (map X ℙ) μ
this : pdf X ℙ μ = 0
refine_2 : ∀ (a : E), Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ pdf X ℙ μ x = 0 x) x} a
refine_2₁ : ∀ (a : E), pdf X ℙ μ a = 0 a
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
filter_upwards using congrFun this

Premises used: congrFun
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
⊢ Measurable (pdf X ℙ μ)

Tactic:
measurable_rnDeriv _ _

Premises used: MeasureTheory.pdf, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
⊢ Measurable (pdf X ℙ μ)

Tactic:
exact measurable_rnDeriv _ _

Premises used: MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
x : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
⊢ μ.withDensity (pdf X ℙ μ) ≤ map X ℙ

Tactic:
withDensity_rnDeriv_le _ _

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_le, MeasureTheory.pdf
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
apply :
  LE.le (α := ℝ≥0∞) ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ ≤ ((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s

Tactic:
apply (withDensity_apply_le _ s).trans

Premises used: MeasureTheory.withDensity_apply_le, LE.le.trans
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
withDensity_pdf_le_map _ _ _ s

Premises used: MeasureTheory.withDensity_pdf_le_map
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact withDensity_pdf_le_map _ _ _ s

Premises used: MeasureTheory.withDensity_pdf_le_map
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
rw : map X ℙ = μ.withDensity (rnDeriv (map X ℙ) μ)
rw₁ rw₂ : Eq (α := Measure E) (map X ℙ) (map X ℙ)
⊢ map X ℙ = μ.withDensity (pdf X ℙ μ)

Tactic:
rw [pdf_def, withDensity_rnDeriv_eq _ _ hX.absolutelyContinuous]

Premises used: MeasureTheory.pdf_def, MeasureTheory.HasPDF.absolutelyContinuous, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
s : Set E
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (pdf X ℙ μ) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s = ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ

Tactic:
rw [← withDensity_apply _ hs, map_eq_withDensity_pdf X ℙ μ]

Premises used: MeasureTheory.map_eq_withDensity_pdf, MeasureTheory.withDensity_apply
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᶠ[ae ℙ] Y
rw : rnDeriv (map X ℙ) μ = pdf Y ℙ μ
rw₁ : rnDeriv (map X ℙ) μ = rnDeriv (map Y ℙ) μ
rw₂ rw₃ : rnDeriv (map Y ℙ) μ = rnDeriv (map Y ℙ) μ
⊢ pdf X ℙ μ = pdf Y ℙ μ

Tactic:
rw [pdf_def, pdf_def, map_congr hXY]

Premises used: MeasureTheory.Measure.map_congr, MeasureTheory.pdf_def
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
rw : ∫⁻ (x : E) in Set.univ, pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ
rw₁ :
  Eq (α := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.univ) : ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
rw₃ rw₄ : Eq (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ = (ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ

Tactic:
rw [← setLIntegral_univ, ← map_eq_setLIntegral_pdf X ℙ μ MeasurableSet.univ,
    map_apply_of_aemeasurable (HasPDF.aemeasurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]

Premises used: MeasureTheory.map_eq_setLIntegral_pdf, MeasureTheory.Measure.map_apply_of_aemeasurable, Set.preimage_univ, MeasureTheory.HasPDF.aemeasurable, MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
rw : μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f
⊢ map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f

Tactic:
rw [map_eq_withDensity_pdf X ℙ μ]

Premises used: MeasureTheory.map_eq_withDensity_pdf
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
apply : ∫⁻ (x : E), pdf X ℙ μ x ∂μ ≠ ∞
⊢ μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f

Tactic:
apply withDensity_eq_iff (measurable_pdf X ℙ μ).aemeasurable hmf

Premises used: Measurable.aemeasurable, MeasureTheory.measurable_pdf, MeasureTheory.withDensity_eq_iff
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
rw : Ne (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ ≠ ∞

Tactic:
rw [lintegral_eq_measure_univ]

Premises used: MeasureTheory.pdf.lintegral_eq_measure_univ
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ Ne (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ Ne (α := ℝ≥0∞) ((ℙ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : SigmaFinite μ
X : Ω → E
inst_2 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f

Tactic:
map_eq_withDensity_pdf X ℙ μ ▸
    withDensity_eq_iff_of_sigmaFinite (measurable_pdf X ℙ μ).aemeasurable hmf

Premises used: Measurable.aemeasurable, Eq.rec, MeasureTheory.measurable_pdf, MeasureTheory.map_eq_withDensity_pdf, MeasureTheory.withDensity_eq_iff_of_sigmaFinite, Eq.symm
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
inst_1 : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ μ x < ∞

Tactic:
rnDeriv_lt_top (map X ℙ) μ

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.pdf, MeasureTheory.Measure.map
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst_1 : IsFiniteMeasure ℙ
X : Ω → E
⊢ (fun (x : E) ↦ ENNReal.ofReal (pdf X ℙ μ x).toReal) =ᶠ[ae μ] pdf X ℙ μ

Tactic:
ofReal_toReal_ae_eq ae_lt_top

Premises used: MeasureTheory.ofReal_toReal_ae_eq, MeasureTheory.pdf.ae_lt_top
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst_1 : HasPDF X ℙ μ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
rw : ∫⁻ (x : E), rnDeriv (map X ℙ) μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
rw₁ : ∫⁻ (x : E), rnDeriv (map X ℙ) μ x * f x ∂μ = ∫⁻ (a : E), f a ∂map X ℙ
rw₂ rw₃ : ∫⁻ (x : E), f x ∂map X ℙ = ∫⁻ (a : E), f a ∂map X ℙ
⊢ ∫⁻ (x : E), pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ

Tactic:
rw [pdf_def,
    ← lintegral_map' (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
    lintegral_rnDeriv_mul HasPDF.absolutelyContinuous hf]

Premises used: MeasureTheory.lintegral_rnDeriv_mul, AEMeasurable.mono_ac, MeasureTheory.pdf_def, MeasureTheory.HasPDF.aemeasurable, MeasureTheory.lintegral_map', MeasureTheory.HasPDF.absolutelyContinuous
-- Module: Mathlib.Probability.Density
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : IsFiniteMeasure ℙ
X : Ω → E
inst_4 : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
rw : @Integrable _ _ _ _ inst f (map X ℙ) ↔ Integrable f (μ.withDensity (rnDeriv (map X ℙ) μ))
⊢ Integrable.{u_3, u_2} (ε := F) (fun (x : E) ↦ (pdf X ℙ μ x).toReal • f x) μ ↔
    Integrable.{u_3, u_1} (ε := F) (fun (x : Ω) ↦ f (X x)) ℙ

Tactic:
rw [← Function.comp_def,
    ← integrable_map_measure (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
    map_eq_withDensity_pdf X ℙ μ, pdf_def, integrable_rnDeriv_smul_iff HasPDF.absolutelyContinuous]

Premises used: MeasureTheory.map_eq_withDensity_pdf, MeasureTheory.AEStronglyMeasurable.mono_ac, Function.comp_def, MeasureTheory.pdf_def, MeasureTheory.integrable_rnDeriv_smul_iff, MeasureTheory.HasPDF.aemeasurable, MeasureTheory.integrable_map_measure, MeasureTheory.HasPDF.absolutelyContinuous