[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬HasPDF X ℙ
⊢ pdf X ℙ = 0
[PROOFSTEP]
simp only [pdf, dif_neg h]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : pdf X ℙ ≠ 0
⊢ HasPDF X ℙ
[PROOFSTEP]
by_contra hpdf
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : pdf X ℙ ≠ 0
hpdf : ¬HasPDF X ℙ
⊢ False
[PROOFSTEP]
simp [pdf, hpdf] at h 
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : pdf X ℙ ≠ 0
⊢ Measurable X
[PROOFSTEP]
by_contra hX
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : pdf X ℙ ≠ 0
hX : ¬Measurable X
⊢ False
[PROOFSTEP]
exact h (pdf_eq_zero_of_not_measurable hX)
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
⊢ Measurable (pdf X ℙ)
[PROOFSTEP]
unfold pdf
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
⊢ Measurable (if hX : HasPDF X ℙ then Classical.choose (_ : ∃ f, Measurable f ∧ map X ℙ = withDensity μ f) else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
h : HasPDF X ℙ
⊢ Measurable (Classical.choose (_ : ∃ f, Measurable f ∧ map X ℙ = withDensity μ f))
case neg
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
h : ¬HasPDF X ℙ
⊢ Measurable 0
[PROOFSTEP]
exacts [(Classical.choose_spec h.1.2).1, measurable_zero]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
hX : HasPDF X ℙ
⊢ map X ℙ = withDensity μ (pdf X ℙ)
[PROOFSTEP]
simp only [pdf, dif_pos hX]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
hX : HasPDF X ℙ
⊢ map X ℙ = withDensity μ (Classical.choose (_ : ∃ f, Measurable f ∧ map X ℙ = withDensity μ f))
[PROOFSTEP]
exact (Classical.choose_spec hX.pdf'.2).2
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
hX : HasPDF X ℙ
s : Set E
hs : MeasurableSet s
⊢ ↑↑(map X ℙ) s = ∫⁻ (x : E) in s, pdf X ℙ x ∂μ
[PROOFSTEP]
rw [← withDensity_apply _ hs, map_eq_withDensity_pdf X ℙ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ
⊢ ∫⁻ (x : E), pdf X ℙ x ∂μ = ↑↑ℙ Set.univ
[PROOFSTEP]
rw [← set_lintegral_univ, ← map_eq_set_lintegral_pdf X ℙ μ MeasurableSet.univ,
  Measure.map_apply (HasPDF.measurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ x < ⊤
[PROOFSTEP]
by_cases hpdf : HasPDF X ℙ μ
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf : HasPDF X ℙ
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ x < ⊤
[PROOFSTEP]
haveI := hpdf
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf this : HasPDF X ℙ
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ x < ⊤
[PROOFSTEP]
refine' ae_lt_top (measurable_pdf X ℙ μ) _
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf this : HasPDF X ℙ
⊢ ∫⁻ (x : E), pdf X ℙ x ∂μ ≠ ⊤
[PROOFSTEP]
rw [lintegral_eq_measure_univ]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf this : HasPDF X ℙ
⊢ ↑↑ℙ Set.univ ≠ ⊤
[PROOFSTEP]
exact (measure_lt_top _ _).ne
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf : ¬HasPDF X ℙ
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ x < ⊤
[PROOFSTEP]
simp [pdf, hpdf]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
⊢ (Integrable fun x => f (X x)) ↔ Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
erw [← integrable_map_measure hf.aestronglyMeasurable (HasPDF.measurable X ℙ μ).aemeasurable,
  map_eq_withDensity_pdf X ℙ μ, integrable_withDensity_iff (measurable_pdf _ _ _) ae_lt_top]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
⊢ ∫ (x : E), f x * ENNReal.toReal (pdf X ℙ x) ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
[PROOFSTEP]
by_cases hpdf : Integrable (fun x => f x * (pdf X ℙ μ x).toReal) μ
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫ (x : E), f x * ENNReal.toReal (pdf X ℙ x) ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
[PROOFSTEP]
rw [← integral_map (HasPDF.measurable X ℙ μ).aemeasurable hf.aestronglyMeasurable, map_eq_withDensity_pdf X ℙ μ,
  integral_eq_lintegral_pos_part_sub_lintegral_neg_part hpdf, integral_eq_lintegral_pos_part_sub_lintegral_neg_part,
  lintegral_withDensity_eq_lintegral_mul _ (measurable_pdf X ℙ μ) hf.neg.ennreal_ofReal,
  lintegral_withDensity_eq_lintegral_mul _ (measurable_pdf X ℙ μ) hf.ennreal_ofReal]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ENNReal.toReal (∫⁻ (a : E), ENNReal.ofReal (f a * ENNReal.toReal (pdf X ℙ a)) ∂μ) -
      ENNReal.toReal (∫⁻ (a : E), ENNReal.ofReal (-(f a * ENNReal.toReal (pdf X ℙ a))) ∂μ) =
    ENNReal.toReal (∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (f x)) a ∂μ) -
      ENNReal.toReal (∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (-f x)) a ∂μ)
[PROOFSTEP]
congr 2
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (f a * ENNReal.toReal (pdf X ℙ a)) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (f x)) a ∂μ
[PROOFSTEP]
have : ∀ x, ENNReal.ofReal (f x * (pdf X ℙ μ x).toReal) = ENNReal.ofReal (pdf X ℙ μ x).toReal * ENNReal.ofReal (f x) :=
  fun x ↦ by rw [mul_comm, ENNReal.ofReal_mul ENNReal.toReal_nonneg]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
x : E
⊢ ENNReal.ofReal (f x * ENNReal.toReal (pdf X ℙ x)) = ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (f x)
[PROOFSTEP]
rw [mul_comm, ENNReal.ofReal_mul ENNReal.toReal_nonneg]
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this :
  ∀ (x : E),
    ENNReal.ofReal (f x * ENNReal.toReal (pdf X ℙ x)) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (f x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (f a * ENNReal.toReal (pdf X ℙ a)) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (f x)) a ∂μ
[PROOFSTEP]
simp_rw [this]
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this :
  ∀ (x : E),
    ENNReal.ofReal (f x * ENNReal.toReal (pdf X ℙ x)) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (f x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (ENNReal.toReal (pdf X ℙ a)) * ENNReal.ofReal (f a) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (f x)) a ∂μ
[PROOFSTEP]
exact lintegral_congr_ae (Filter.EventuallyEq.mul ofReal_toReal_ae_eq (ae_eq_refl _))
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (-(f a * ENNReal.toReal (pdf X ℙ a))) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (-f x)) a ∂μ
[PROOFSTEP]
have :
  ∀ x, ENNReal.ofReal (-(f x * (pdf X ℙ μ x).toReal)) = ENNReal.ofReal (pdf X ℙ μ x).toReal * ENNReal.ofReal (-f x) :=
  by
  intro x
  rw [neg_mul_eq_neg_mul, mul_comm, ENNReal.ofReal_mul ENNReal.toReal_nonneg]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∀ (x : E),
    ENNReal.ofReal (-(f x * ENNReal.toReal (pdf X ℙ x))) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (-f x)
[PROOFSTEP]
intro x
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
x : E
⊢ ENNReal.ofReal (-(f x * ENNReal.toReal (pdf X ℙ x))) =
    ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (-f x)
[PROOFSTEP]
rw [neg_mul_eq_neg_mul, mul_comm, ENNReal.ofReal_mul ENNReal.toReal_nonneg]
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this :
  ∀ (x : E),
    ENNReal.ofReal (-(f x * ENNReal.toReal (pdf X ℙ x))) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (-f x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (-(f a * ENNReal.toReal (pdf X ℙ a))) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (-f x)) a ∂μ
[PROOFSTEP]
simp_rw [this]
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this :
  ∀ (x : E),
    ENNReal.ofReal (-(f x * ENNReal.toReal (pdf X ℙ x))) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (-f x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (ENNReal.toReal (pdf X ℙ a)) * ENNReal.ofReal (-f a) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (-f x)) a ∂μ
[PROOFSTEP]
exact lintegral_congr_ae (Filter.EventuallyEq.mul ofReal_toReal_ae_eq (ae_eq_refl _))
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ Integrable fun y => f y
[PROOFSTEP]
refine' ⟨hf.aestronglyMeasurable, _⟩
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ HasFiniteIntegral fun y => f y
[PROOFSTEP]
rw [HasFiniteIntegral, lintegral_withDensity_eq_lintegral_mul _ (measurable_pdf _ _ _) hf.nnnorm.coe_nnreal_ennreal]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫⁻ (a : E), (pdf X ℙ * fun x => ↑‖f x‖₊) a ∂μ < ⊤
[PROOFSTEP]
have : (fun x => (pdf X ℙ μ * fun x => (‖f x‖₊ : ℝ≥0∞)) x) =ᵐ[μ] fun x => ‖f x * (pdf X ℙ μ x).toReal‖₊ :=
  by
  simp_rw [← smul_eq_mul, nnnorm_smul, ENNReal.coe_mul]
  rw [smul_eq_mul, mul_comm]
  refine' Filter.EventuallyEq.mul (ae_eq_refl _) (ae_eq_trans ofReal_toReal_ae_eq.symm _)
  simp only [Real.ennnorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ (fun x => (pdf X ℙ * fun x => ↑‖f x‖₊) x) =ᶠ[ae μ] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
simp_rw [← smul_eq_mul, nnnorm_smul, ENNReal.coe_mul]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ (fun x => (pdf X ℙ • fun x => ↑‖f x‖₊) x) =ᶠ[ae μ] fun x => ↑‖f x‖₊ * ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
rw [smul_eq_mul, mul_comm]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ (fun x => ((fun x => ↑‖f x‖₊) * pdf X ℙ) x) =ᶠ[ae μ] fun x => ↑‖f x‖₊ * ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
refine' Filter.EventuallyEq.mul (ae_eq_refl _) (ae_eq_trans ofReal_toReal_ae_eq.symm _)
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ (fun x => ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x))) =ᶠ[ae μ] fun x => ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
simp only [Real.ennnorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this : (fun x => (pdf X ℙ * fun x => ↑‖f x‖₊) x) =ᶠ[ae μ] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
⊢ ∫⁻ (a : E), (pdf X ℙ * fun x => ↑‖f x‖₊) a ∂μ < ⊤
[PROOFSTEP]
rw [lintegral_congr_ae this]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this : (fun x => (pdf X ℙ * fun x => ↑‖f x‖₊) x) =ᶠ[ae μ] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
⊢ ∫⁻ (a : E), ↑‖f a * ENNReal.toReal (pdf X ℙ a)‖₊ ∂μ < ⊤
[PROOFSTEP]
exact hpdf.2
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : ¬Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫ (x : E), f x * ENNReal.toReal (pdf X ℙ x) ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
[PROOFSTEP]
rw [integral_undef hpdf, integral_undef]
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : ¬Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ¬Integrable fun x => f (X x)
[PROOFSTEP]
rwa [← integrable_iff_integrable_mul_pdf hf] at hpdf 
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ
⊢ map X ℙ ≪ μ
[PROOFSTEP]
rw [map_eq_withDensity_pdf X ℙ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ
⊢ withDensity μ (pdf X ℙ) ≪ μ
[PROOFSTEP]
exact withDensity_absolutelyContinuous _ _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX' : HasPDF X ℙ
⊢ Measurable (0, pdf X ℙ).snd ∧ (0, pdf X ℙ).fst ⟂ₘ μ ∧ map X ℙ = (0, pdf X ℙ).fst + withDensity μ (0, pdf X ℙ).snd
[PROOFSTEP]
simp only [zero_add, measurable_pdf X ℙ μ, true_and_iff, MutuallySingular.zero_left, map_eq_withDensity_pdf X ℙ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
⊢ HasPDF X ℙ ↔ Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
constructor
[GOAL]
case mp
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
⊢ HasPDF X ℙ → Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
intro hX'
[GOAL]
case mp
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX' : HasPDF X ℙ
⊢ Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
exact ⟨hX'.pdf'.1, haveLebesgueDecomposition_of_hasPDF, map_absolutelyContinuous⟩
[GOAL]
case mpr
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
⊢ Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ → HasPDF X ℙ
[PROOFSTEP]
rintro ⟨hX, h_decomp, h⟩
[GOAL]
case mpr.intro.intro
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
h_decomp : HaveLebesgueDecomposition (map X ℙ) μ
h : map X ℙ ≪ μ
⊢ HasPDF X ℙ
[PROOFSTEP]
haveI := h_decomp
[GOAL]
case mpr.intro.intro
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
h_decomp : HaveLebesgueDecomposition (map X ℙ) μ
h : map X ℙ ≪ μ
this : HaveLebesgueDecomposition (map X ℙ) μ
⊢ HasPDF X ℙ
[PROOFSTEP]
refine' ⟨⟨hX, (Measure.map X ℙ).rnDeriv μ, measurable_rnDeriv _ _, _⟩⟩
[GOAL]
case mpr.intro.intro
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
h_decomp : HaveLebesgueDecomposition (map X ℙ) μ
h : map X ℙ ≪ μ
this : HaveLebesgueDecomposition (map X ℙ) μ
⊢ map X ℙ = withDensity μ (rnDeriv (map X ℙ) μ)
[PROOFSTEP]
rwa [withDensity_rnDeriv_eq]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
⊢ HasPDF X ℙ ↔ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
rw [hasPDF_iff]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
⊢ Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ ↔
    HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
simp only [hX, true_and]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ HasPDF (g ∘ X) ℙ
[PROOFSTEP]
rw [hasPDF_iff, ← map_map hg.measurable (HasPDF.measurable X ℙ μ)]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ Measurable (g ∘ X) ∧ HaveLebesgueDecomposition (map g (map X ℙ)) ν ∧ map g (map X ℙ) ≪ ν
[PROOFSTEP]
refine' ⟨hg.measurable.comp (HasPDF.measurable X ℙ μ), hmap, _⟩
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ map g (map X ℙ) ≪ ν
[PROOFSTEP]
rw [map_eq_withDensity_pdf X ℙ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ map g (withDensity μ (pdf X ℙ)) ≪ ν
[PROOFSTEP]
refine' AbsolutelyContinuous.mk fun s hsm hs => _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
s : Set F
hsm : MeasurableSet s
hs : ↑↑ν s = 0
⊢ ↑↑(map g (withDensity μ (pdf X ℙ))) s = 0
[PROOFSTEP]
rw [map_apply hg.measurable hsm, withDensity_apply _ (hg.measurable hsm)]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
s : Set F
hsm : MeasurableSet s
hs : ↑↑ν s = 0
⊢ ∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ a ∂μ = 0
[PROOFSTEP]
have := hg.absolutelyContinuous hs
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
s : Set F
hsm : MeasurableSet s
hs : ↑↑ν s = 0
this : ↑↑(map g μ) s = 0
⊢ ∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ a ∂μ = 0
[PROOFSTEP]
rw [map_apply hg.measurable hsm] at this 
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
s : Set F
hsm : MeasurableSet s
hs : ↑↑ν s = 0
this : ↑↑μ (g ⁻¹' s) = 0
⊢ ∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ a ∂μ = 0
[PROOFSTEP]
exact set_lintegral_measure_zero _ _ this
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Measurable X
⊢ HasPDF X ℙ ↔ map X ℙ ≪ volume
[PROOFSTEP]
rw [hasPDF_iff_of_measurable hX]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Measurable X
⊢ HaveLebesgueDecomposition (map X ℙ) volume ∧ map X ℙ ≪ volume ↔ map X ℙ ≪ volume
[PROOFSTEP]
exact and_iff_right inferInstance
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
⊢ HasPDF X ℙ ↔ Measurable X ∧ map X ℙ ≪ volume
[PROOFSTEP]
by_cases hX : Measurable X
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Measurable X
⊢ HasPDF X ℙ ↔ Measurable X ∧ map X ℙ ≪ volume
[PROOFSTEP]
rw [Real.hasPDF_iff_of_measurable hX, iff_and_self]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Measurable X
⊢ map X ℙ ≪ volume → Measurable X
[PROOFSTEP]
exact fun _ => hX
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : ¬Measurable X
⊢ HasPDF X ℙ ↔ Measurable X ∧ map X ℙ ≪ volume
[PROOFSTEP]
exact ⟨fun h => False.elim (hX h.pdf'.1), fun h => False.elim (hX h.1)⟩
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ HasFiniteIntegral fun x => f x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
rw [HasFiniteIntegral]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ ∫⁻ (a : ℝ), ↑‖f a * ENNReal.toReal (pdf X ℙ a)‖₊ < ⊤
[PROOFSTEP]
have : (fun x => ↑‖f x‖₊ * g x) =ᵐ[volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖₊ :=
  by
  refine'
    ae_eq_trans
      (Filter.EventuallyEq.mul (ae_eq_refl fun x => (‖f x‖₊ : ℝ≥0∞)) (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) _
  simp_rw [← smul_eq_mul, nnnorm_smul, ENNReal.coe_mul, smul_eq_mul]
  refine' Filter.EventuallyEq.mul (ae_eq_refl _) _
  simp only [Real.ennnorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ (fun x => ↑‖f x‖₊ * g x) =ᶠ[ae volume] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
refine'
  ae_eq_trans
    (Filter.EventuallyEq.mul (ae_eq_refl fun x => (‖f x‖₊ : ℝ≥0∞)) (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ (fun x => ↑‖f x‖₊ * ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x))) =ᶠ[ae volume] fun x =>
    ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
simp_rw [← smul_eq_mul, nnnorm_smul, ENNReal.coe_mul, smul_eq_mul]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ (fun x => ↑‖f x‖₊ * ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x))) =ᶠ[ae volume] fun x =>
    ↑‖f x‖₊ * ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
refine' Filter.EventuallyEq.mul (ae_eq_refl _) _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ (fun x => ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x))) =ᶠ[ae volume] fun x => ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
simp only [Real.ennnorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
this : (fun x => ↑‖f x‖₊ * g x) =ᶠ[ae volume] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
⊢ ∫⁻ (a : ℝ), ↑‖f a * ENNReal.toReal (pdf X ℙ a)‖₊ < ⊤
[PROOFSTEP]
rwa [lt_top_iff_ne_top, ← lintegral_congr_ae this]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hu : IsUniform X s ℙ
⊢ pdf X ℙ ≠ 0
[PROOFSTEP]
intro hpdf
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hu : IsUniform X s ℙ
hpdf : pdf X ℙ = 0
⊢ False
[PROOFSTEP]
simp only [IsUniform, hpdf] at hu 
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
⊢ False
[PROOFSTEP]
suffices μ (s ∩ Function.support ((μ s)⁻¹ • (1 : E → ℝ≥0∞))) = 0
  by
  have heq : Function.support ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) = Set.univ :=
    by
    ext x
    rw [Function.mem_support]
    simp [hnt]
  rw [heq, Set.inter_univ] at this 
  exact hns this
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
⊢ False
[PROOFSTEP]
have heq : Function.support ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) = Set.univ :=
  by
  ext x
  rw [Function.mem_support]
  simp [hnt]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
⊢ Function.support ((↑↑μ s)⁻¹ • 1) = Set.univ
[PROOFSTEP]
ext x
[GOAL]
case h
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
x : E
⊢ x ∈ Function.support ((↑↑μ s)⁻¹ • 1) ↔ x ∈ Set.univ
[PROOFSTEP]
rw [Function.mem_support]
[GOAL]
case h
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
x : E
⊢ ((↑↑μ s)⁻¹ • 1) x ≠ 0 ↔ x ∈ Set.univ
[PROOFSTEP]
simp [hnt]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
heq : Function.support ((↑↑μ s)⁻¹ • 1) = Set.univ
⊢ False
[PROOFSTEP]
rw [heq, Set.inter_univ] at this 
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ s = 0
heq : Function.support ((↑↑μ s)⁻¹ • 1) = Set.univ
⊢ False
[PROOFSTEP]
exact hns this
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
⊢ ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
[PROOFSTEP]
exact Set.indicator_ae_eq_zero.1 hu.symm
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
A : Set E
hA : MeasurableSet A
⊢ ↑↑ℙ (X ⁻¹' A) = ↑↑μ (s ∩ A) / ↑↑μ s
[PROOFSTEP]
haveI := hu.hasPDF hns hnt
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
A : Set E
hA : MeasurableSet A
this : HasPDF X ℙ
⊢ ↑↑ℙ (X ⁻¹' A) = ↑↑μ (s ∩ A) / ↑↑μ s
[PROOFSTEP]
rw [← Measure.map_apply (HasPDF.measurable X ℙ μ) hA, map_eq_set_lintegral_pdf X ℙ μ hA, lintegral_congr_ae hu.restrict]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
A : Set E
hA : MeasurableSet A
this : HasPDF X ℙ
⊢ ∫⁻ (a : E) in A, Set.indicator s ((↑↑μ s)⁻¹ • 1) a ∂μ = ↑↑μ (s ∩ A) / ↑↑μ s
[PROOFSTEP]
simp only [hms, hA, lintegral_indicator, Pi.smul_apply, Pi.one_apply, Algebra.id.smul_eq_mul, mul_one, lintegral_const,
  restrict_apply', Set.univ_inter]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
A : Set E
hA : MeasurableSet A
this : HasPDF X ℙ
⊢ (↑↑μ s)⁻¹ * ↑↑μ (s ∩ A) = ↑↑μ (s ∩ A) / ↑↑μ s
[PROOFSTEP]
rw [ENNReal.div_eq_inv_mul]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
⊢ ↑↑ℙ Set.univ = 1
[PROOFSTEP]
have : X ⁻¹' Set.univ = Set.univ := by simp only [Set.preimage_univ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
⊢ X ⁻¹' Set.univ = Set.univ
[PROOFSTEP]
simp only [Set.preimage_univ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
this : X ⁻¹' Set.univ = Set.univ
⊢ ↑↑ℙ Set.univ = 1
[PROOFSTEP]
rw [← this, hu.measure_preimage hns hnt hms MeasurableSet.univ, Set.inter_univ, ENNReal.div_self hns hnt]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
⊢ Integrable fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
by_cases hsupp : volume s = ∞
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
⊢ Integrable fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
have : pdf X ℙ =ᵐ[volume] 0 := by
  refine' ae_eq_trans huX _
  simp [hsupp, ae_eq_refl]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
⊢ pdf X ℙ =ᶠ[ae volume] 0
[PROOFSTEP]
refine' ae_eq_trans huX _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
⊢ Set.indicator s ((↑↑volume s)⁻¹ • 1) =ᶠ[ae volume] 0
[PROOFSTEP]
simp [hsupp, ae_eq_refl]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
this : pdf X ℙ =ᶠ[ae volume] 0
⊢ Integrable fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
refine' Integrable.congr (integrable_zero _ _ _) _
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
this : pdf X ℙ =ᶠ[ae volume] 0
⊢ (fun x => 0) =ᶠ[ae volume] fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
rw [(by simp : (fun x => 0 : ℝ → ℝ) = fun x => x * (0 : ℝ≥0∞).toReal)]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
this : pdf X ℙ =ᶠ[ae volume] 0
⊢ (fun x => 0) = fun x => x * ENNReal.toReal 0
[PROOFSTEP]
simp
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
this : pdf X ℙ =ᶠ[ae volume] 0
⊢ (fun x => x * ENNReal.toReal 0) =ᶠ[ae volume] fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
refine' Filter.EventuallyEq.mul (ae_eq_refl _) (Filter.EventuallyEq.fun_comp this.symm ENNReal.toReal)
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
⊢ Integrable fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
constructor
  -- porting note: `refine` was failing, don't know why
[GOAL]
case neg.left
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
⊢ AEStronglyMeasurable (fun x => x * ENNReal.toReal (pdf X ℙ x)) volume
[PROOFSTEP]
exact aestronglyMeasurable_id.mul (measurable_pdf X ℙ).aemeasurable.ennreal_toReal.aestronglyMeasurable
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
⊢ HasFiniteIntegral fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
refine' hasFiniteIntegral_mul huX _
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
⊢ ∫⁻ (x : ℝ), ↑‖x‖₊ * Set.indicator s ((↑↑volume s)⁻¹ • 1) x ≠ ⊤
[PROOFSTEP]
set ind := (volume s)⁻¹ • (1 : ℝ → ℝ≥0∞)
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
ind : ℝ → ℝ≥0∞ := (↑↑volume s)⁻¹ • 1
⊢ ∫⁻ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x ≠ ⊤
[PROOFSTEP]
have : ∀ x, ↑‖x‖₊ * s.indicator ind x = s.indicator (fun x => ‖x‖₊ * ind x) x := fun x =>
  (s.indicator_mul_right (fun x => ↑‖x‖₊) ind).symm
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
ind : ℝ → ℝ≥0∞ := (↑↑volume s)⁻¹ • 1
this : ∀ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x = Set.indicator s (fun x => ↑‖x‖₊ * ind x) x
⊢ ∫⁻ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x ≠ ⊤
[PROOFSTEP]
simp only [this, lintegral_indicator _ hms, mul_one, Algebra.id.smul_eq_mul, Pi.one_apply, Pi.smul_apply]
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
ind : ℝ → ℝ≥0∞ := (↑↑volume s)⁻¹ • 1
this : ∀ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x = Set.indicator s (fun x => ↑‖x‖₊ * ind x) x
⊢ ∫⁻ (x : ℝ) in s, ↑‖x‖₊ * (↑↑volume s)⁻¹ ≠ ⊤
[PROOFSTEP]
rw [lintegral_mul_const _ measurable_nnnorm.coe_nnreal_ennreal]
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
ind : ℝ → ℝ≥0∞ := (↑↑volume s)⁻¹ • 1
this : ∀ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x = Set.indicator s (fun x => ↑‖x‖₊ * ind x) x
⊢ (∫⁻ (a : ℝ) in s, ↑‖a‖₊) * (↑↑volume s)⁻¹ ≠ ⊤
[PROOFSTEP]
refine'
  (ENNReal.mul_lt_top (set_lintegral_lt_top_of_isCompact hsupp hcs continuous_nnnorm).ne
      (ENNReal.inv_lt_top.2 (pos_iff_ne_zero.mpr hns)).ne).ne
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
haveI := hasPDF hns hnt huX
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this : HasPDF X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
haveI := huX.isProbabilityMeasure hns hnt hms
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
rw [← integral_mul_eq_integral]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
⊢ ∫ (x : ℝ), x * ENNReal.toReal (pdf (fun x => X x) ℙ x) = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
rw [integral_congr_ae (Filter.EventuallyEq.mul (ae_eq_refl _) (pdf_toReal_ae_eq huX))]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
⊢ ∫ (a : ℝ), a * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) a) =
    ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
have :
  ∀ x,
    x * (s.indicator ((volume s)⁻¹ • (1 : ℝ → ℝ≥0∞)) x).toReal =
      x * s.indicator ((volume s)⁻¹.toReal • (1 : ℝ → ℝ)) x :=
  by
  refine' fun x => congr_arg ((· * ·) x) _
  by_cases hx : x ∈ s
  · simp [Set.indicator_of_mem hx]
  · simp [Set.indicator_of_not_mem hx]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
⊢ ∀ (x : ℝ),
    x * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) =
      x * Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
[PROOFSTEP]
refine' fun x => congr_arg ((· * ·) x) _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
x : ℝ
⊢ ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) = Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
x : ℝ
hx : x ∈ s
⊢ ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) = Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
[PROOFSTEP]
simp [Set.indicator_of_mem hx]
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
x : ℝ
hx : ¬x ∈ s
⊢ ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) = Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
[PROOFSTEP]
simp [Set.indicator_of_not_mem hx]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝¹ : HasPDF X ℙ
this✝ : IsProbabilityMeasure ℙ
this :
  ∀ (x : ℝ),
    x * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) =
      x * Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
⊢ ∫ (a : ℝ), a * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) a) =
    ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
simp_rw [this, ← s.indicator_mul_right fun x => x, integral_indicator hms]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝¹ : HasPDF X ℙ
this✝ : IsProbabilityMeasure ℙ
this :
  ∀ (x : ℝ),
    x * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) =
      x * Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
⊢ ∫ (a : ℝ) in s, a * (ENNReal.toReal (↑↑volume s)⁻¹ • 1) a = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
change ∫ x in s, x * (volume s)⁻¹.toReal • (1 : ℝ) = _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝¹ : HasPDF X ℙ
this✝ : IsProbabilityMeasure ℙ
this :
  ∀ (x : ℝ),
    x * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) =
      x * Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
⊢ ∫ (x : ℝ) in s, x * ENNReal.toReal (↑↑volume s)⁻¹ • 1 = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
rw [integral_mul_right, mul_comm, smul_eq_mul, mul_one]
