-- Mathlib/Probability/Distributions/Uniform.lean
theorem mul_pdf_integrable (hcs : IsCompact s) (huX : IsUniform X s ℙ) :
    Integrable fun x : ℝ => x * (pdf X ℙ volume x).toReal

Proof state:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x
⊢ ∫⁻ (x : ℝ) in s, ‖x‖ₑ * (volume s)⁻¹ ∂volume ≠ ⊤

Tactic:
rw [lintegral_mul_const _ measurable_enorm]

Result:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x
⊢ (∫⁻ (a : ℝ) in s, ‖a‖ₑ ∂volume) * (volume s)⁻¹ ≠ ⊤

Proof state:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

Tactic:
by_cases hnt : volume s = 0 ∨ volume s = ∞

Result:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬(volume s = 0 ∨ volume s = ⊤)
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

Proof state:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ⊤

Tactic:
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

Result:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ⊤

Proof state:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ⊤

Tactic:
simp only [ind, this, lintegral_indicator hcs.measurableSet, mul_one, Algebra.id.smul_eq_mul,
  Pi.one_apply, Pi.smul_apply]

Result:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x
⊢ ∫⁻ (x : ℝ) in s, ‖x‖ₑ * (volume s)⁻¹ ∂volume ≠ ⊤

Proof state:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
I : Integrable (fun x => x * ENNReal.toReal 0) volume
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

Tactic:
apply I.congr

Result:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
I : Integrable (fun x => x * ENNReal.toReal 0) volume
⊢ (fun x => x * ENNReal.toReal 0) =ᶠ[ae volume] fun x => x * (pdf X ℙ volume x).toReal

Proof state:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬(volume s = 0 ∨ volume s = ⊤)
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

Tactic:
simp only [not_or] at hnt

Result:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

Proof state:
case h
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
I : Integrable (fun x => x * ENNReal.toReal 0) volume
x : ℝ
hx : pdf X ℙ volume x = 0 x
⊢ x * ENNReal.toReal 0 = x * (pdf X ℙ volume x).toReal

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
⊢ HasFiniteIntegral (fun x => x * (pdf X ℙ volume x).toReal) volume

Tactic:
refine hasFiniteIntegral_mul (pdf_eq hcs.measurableSet huX) ?_

Result:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ((volume s)⁻¹ • 1) x ≠ ⊤

Proof state:
case neg.left
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
⊢ AEStronglyMeasurable (fun x => x * (pdf X ℙ volume x).toReal) volume

Tactic:
exact aestronglyMeasurable_id.mul
  (measurable_pdf X ℙ).aemeasurable.ennreal_toReal.aestronglyMeasurable

Result:
no goals

Proof state:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ((volume s)⁻¹ • 1) x ≠ ⊤

Tactic:
set ind := (volume s)⁻¹ • (1 : ℝ → ℝ≥0∞)

Result:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ⊤

Proof state:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ⊤
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x
⊢ (∫⁻ (a : ℝ) in s, ‖a‖ₑ ∂volume) * (volume s)⁻¹ ≠ ⊤

Tactic:
exact ENNReal.mul_ne_top (setLIntegral_lt_top_of_isCompact hnt.2 hcs continuous_nnnorm).ne
  (ENNReal.inv_lt_top.2 (pos_iff_ne_zero.mpr hnt.1)).ne

Result:
no goals

Proof state:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
⊢ Integrable (fun x => x * ENNReal.toReal 0) volume

Tactic:
simp

Result:
no goals

Proof state:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume

Tactic:
have I : Integrable (fun x ↦ x * ENNReal.toReal (0)) := by simp

Result:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ⊤
I : Integrable (fun x => x * ENNReal.toReal 0) volume
⊢ Integrable (fun x => x * (pdf X ℙ volume x).toReal) volume