awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖f x‖ₑ * g x) fun (x : ℝ) ↦
    ‖f x * (pdf X ℙ volume x).toReal‖ₑ
have refine : (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal)
  fun (x : ℝ) ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ
Tactic: refine ae_eq_trans ((ae_eq_refl _).fun_mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) fun (x : ℝ) ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ
have simp_rw : (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal)
  fun (x : ℝ) ↦ ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ
Tactic: simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ℝ) ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) fun (x : ℝ) ↦
    ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ
have refine : (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (i : ℝ) ↦ ENNReal.ofReal (pdf X ℙ volume i).toReal)
  fun (x : ℝ) ↦ ‖(pdf X ℙ volume x).toReal‖ₑ
Tactic: refine .fun_mul (ae_eq_refl _) ?_
-- Lean 4 proof step from Mathlib.Probability.Density (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ∞
have this : (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖f x‖ₑ * g x) fun (x : ℝ) ↦
  ‖f x * (pdf X ℙ volume x).toReal‖ₑ
Tactic: have : (fun x => ‖f x‖ₑ * g x) =ᵐ[volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖ₑ := by
    refine ae_eq_trans ((ae_eq_refl _).fun_mul (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) ?_
    simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]
    refine .fun_mul (ae_eq_refl _) ?_
    simp only [Real.enorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᶠ[ae (F := Measure ℝ) volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
this :
  (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖f x‖ₑ * g x) fun (x : ℝ) ↦
    ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ∞
have rwa : ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ ≠ ∞
Tactic: rwa [lt_top_iff_ne_top, ← lintegral_congr_ae this]
-- Lean 4 proof step from Mathlib.Probability.Density (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
⊢ X ⟂ᵢ[ℙ] Y ↔
    pdf (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
have this : HasPDF X ℙ μ
Tactic: have : HasPDF X ℙ μ := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
    quasiMeasurePreserving_fst
-- Lean 4 proof step from Mathlib.Probability.Density (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this : HasPDF X ℙ μ
⊢ X ⟂ᵢ[ℙ] Y ↔
    pdf (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
have this₁ : HasPDF Y ℙ ν
Tactic: have : HasPDF Y ℙ ν := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
    quasiMeasurePreserving_snd
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 : (a : Set (E × F)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
have rw : ∫⁻ (a : E × F) in s ×ˢ t, pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂μ.prod ν =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
      lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
      map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (a : E × F) in s ×ˢ t, pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂μ.prod ν =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ((μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 : (a : Set (E × F)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : ∫⁻ (a : E × F), pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂(μ.restrict s).prod (ν.restrict t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
      lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
      map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (a : E × F) in s ×ˢ t, pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂μ.prod ν =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  ∫⁻ (a : E × F), pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂(μ.restrict s).prod (ν.restrict t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ((μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 : (a : Set (E × F)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
      lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
      map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (a : E × F) in s ×ˢ t, pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂μ.prod ν =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  ∫⁻ (a : E × F), pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂(μ.restrict s).prod (ν.restrict t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ :
  (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ((μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 : (a : Set (E × F)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
have rw₃ : (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
  HMul.hMul (β := ℝ≥0∞) (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
      lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
      map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (a : E × F) in s ×ˢ t, pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂μ.prod ν =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  ∫⁻ (a : E × F), pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂(μ.restrict s).prod (ν.restrict t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ :
  (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
rw₃ :
  (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
    HMul.hMul (β := ℝ≥0∞) (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ((μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 : (a : Set (E × F)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map X ℙ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((map Y ℙ : Measure F) : (a : Set F) → ℝ≥0∞) t : ℝ≥0∞)
have rw₄ : (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
  (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (x : F) in t, pdf Y ℙ ν x ∂ν
Tactic: rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
      lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
      map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]
-- Lean 4 proof step from Mathlib.Probability.Density (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
⊢ X ⟂ᵢ[ℙ] Y ↔
    pdf (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
have h₀ : Measure.prod (map X ℙ) (map Y ℙ) = (μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
Tactic: have h₀ : (ℙ.map X).prod (ℙ.map Y) =
      (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 :=
    prod_eq fun s t hs ht ↦ by rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
      lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
      map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst_1 : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst_2 : IsFiniteMeasure ℙ
inst_3 : SigmaFinite μ
inst_4 : SigmaFinite ν
inst_5 : HasPDF (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this_1 : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : Measure.prod (map X ℙ) (map Y ℙ) = (μ.prod ν).withDensity fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ X ⟂ᵢ[ℙ] Y ↔
    pdf (fun (ω : Ω) ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
have hmf : AEMeasurable (β := ℝ≥0∞) (fun (z : E × F) ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map (HasPDF.aemeasurable X ℙ μ) (HasPDF.aemeasurable Y ℙ ν),
    ← eq_of_map_eq_withDensity, h₀]
-- Lean 4 proof step from Mathlib.Probability.Density (hypothesis)
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
⊢ HasPDF (X * Y) ℙ μ
have this : AEMeasurable X ℙ
Tactic: have : AEMeasurable X ℙ := HasPDF.aemeasurable' μ
-- Lean 4 proof step from Mathlib.Probability.Density (hypothesis)
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 : AEMeasurable X ℙ
⊢ HasPDF (X * Y) ℙ μ
have this₁ : AEMeasurable Y ℙ
Tactic: have : AEMeasurable Y ℙ := HasPDF.aemeasurable' μ
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ
⊢ HasPDF (X * Y) ℙ μ
have rw : HaveLebesgueDecomposition (map X ℙ ∗ₘ map Y ℙ) μ ∧ map X ℙ ∗ₘ map 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]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ ≪ μ
have refine : HaveLebesgueDecomposition (map X ℙ ∗ₘ map Y ℙ) μ
Tactic: refine ⟨?_, mconv_absolutelyContinuous HasPDF.absolutelyContinuous⟩
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ) μ
have hν₁ : map X ℙ ≪ μ
Tactic: apply HaveLebesgueDecomposition.mconv
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ ≪ μ
⊢ HaveLebesgueDecomposition (map X ℙ ∗ₘ map Y ℙ) μ
have hν₂ : map Y ℙ ≪ μ
Tactic: apply HaveLebesgueDecomposition.mconv
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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
⊢ HasPDF (X * Y) ℙ μ
have σX : SigmaFinite (m0 := mG) (map X ℙ)
Tactic: apply hXY.mul_hasPDF'
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ)
⊢ HasPDF (X * Y) ℙ μ
have σY : SigmaFinite (m0 := mG) (map Y ℙ)
Tactic: apply hXY.mul_hasPDF'
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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
⊢ pdf (X * Y) ℙ μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
have rw : rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
Tactic: rw [pdf, hXY.map_mul_eq_map_mconv_map₀' (HasPDF.aemeasurable' μ) (HasPDF.aemeasurable' μ) σX σY]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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
⊢ rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
have hν₁ : map X ℙ ≪ μ
Tactic: apply rnDeriv_mconv'
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ ≪ μ
⊢ rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
have hν₂ : map Y ℙ ≪ μ
Tactic: apply rnDeriv_mconv'
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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
⊢ pdf (X * Y) ℙ μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
have rw : rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
Tactic: rw [pdf, hXY.map_mul_eq_map_mconv_map₀ (HasPDF.aemeasurable' μ) (HasPDF.aemeasurable' μ)]
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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
⊢ rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
have hν₁ : map X ℙ ≪ μ
Tactic: apply rnDeriv_mconv
-- Lean 4 proof step from Mathlib.Probability.Density (goal)
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 ℙ ≪ μ
⊢ rnDeriv (map X ℙ ∗ₘ map Y ℙ) μ =ᶠ[ae μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
have hν₂ : map Y ℙ ≪ μ
Tactic: apply rnDeriv_mconv
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ beta α β = ((↑α : ℂ).betaIntegral (↑β : ℂ)).re
have rw : beta α β = (Gamma (↑α : ℂ) * Gamma (↑β : ℂ) / Gamma ((↑α : ℂ) + (↑β : ℂ))).re
Tactic: rw [betaIntegral_eq_Gamma_mul_div]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
rw : beta α β = (Gamma (↑α : ℂ) * Gamma (↑β : ℂ) / Gamma ((↑α : ℂ) + (↑β : ℂ))).re
⊢ beta α β = ((↑α : ℂ).betaIntegral (↑β : ℂ)).re
have hu : 0 < (↑α : ℂ).re
Tactic: rw [betaIntegral_eq_Gamma_mul_div]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
rw : beta α β = (Gamma (↑α : ℂ) * Gamma (↑β : ℂ) / Gamma ((↑α : ℂ) + (↑β : ℂ))).re
hu : 0 < (↑α : ℂ).re
⊢ beta α β = ((↑α : ℂ).betaIntegral (↑β : ℂ)).re
have hv : 0 < (↑β : ℂ).re
Tactic: rw [betaIntegral_eq_Gamma_mul_div]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ beta α β = (Gamma (↑α : ℂ) * Gamma (↑β : ℂ) / Gamma ((↑α : ℂ) + (↑β : ℂ))).re
have simp_rw : Real.Gamma α * Real.Gamma β / Real.Gamma (α + β) =
  ((↑(Real.Gamma α) : ℂ) * (↑(Real.Gamma β) : ℂ) / (↑(Real.Gamma (α + β)) : ℂ)).re
Tactic: simp_rw [beta, ← ofReal_add α β, Gamma_ofReal]