awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ AEMeasurable (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)) μ

Tactic:
(measurable_one.aemeasurable.const_smul (μ s)⁻¹).indicator hms

Premises used: AEMeasurable.const_smul, Measurable.aemeasurable, AEMeasurable.indicator, measurable_one, Inv.inv, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hns : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ AEMeasurable (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1)) μ

Tactic:
exact (measurable_one.aemeasurable.const_smul (μ s)⁻¹).indicator hms

Premises used: AEMeasurable.const_smul, Measurable.aemeasurable, AEMeasurable.indicator, measurable_one, Inv.inv, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hX : IsUniform X s ℙ μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x_1 : E) ↦ (pdf X ℙ μ x_1).toReal) fun (x : E) ↦
    (s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := E → ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1) x).toReal

Tactic:
Filter.EventuallyEq.fun_comp (pdf_eq hms hX) ENNReal.toReal

Premises used: MeasureTheory.pdf.IsUniform.pdf_eq, ENNReal.toReal, Filter.EventuallyEq.fun_comp, NNReal.toReal
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
pos :
  ∀
    (hnt :
      Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
neg :
  ∀
    (hnt :
      ¬(Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
          Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume

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

Premises used: MeasureTheory.MeasureSpace.volume, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * ENNReal.toReal 0) volume

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * ENNReal.toReal 0) volume

Tactic:
have I : Integrable (fun x ↦ x * ENNReal.toReal (0)) := by simp
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * ENNReal.toReal 0) volume
pos :
  (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ x * ENNReal.toReal 0) fun (x_1 : ℝ) ↦
    x_1 * (pdf X ℙ volume x_1).toReal
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume

Tactic:
apply I.congr

Premises used: MeasureTheory.Integrable.congr
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * ENNReal.toReal 0) volume
h : ∀ (x_1 : ℝ) (hx : pdf X ℙ volume x_1 = 0 x_1), x_1 * ENNReal.toReal 0 = x_1 * (pdf X ℙ volume x_1).toReal
⊢ (ae (F := Measure ℝ) volume).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ x * ENNReal.toReal 0) fun (x_1 : ℝ) ↦
    x_1 * (pdf X ℙ volume x_1).toReal

Tactic:
filter_upwards [pdf_eq_zero_of_measure_eq_zero_or_top huX hnt] with x hx

Premises used: MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x_1 : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (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]
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬(Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [not_or] at hnt

Premises used: not_or
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsProbabilityMeasure ℙ

Tactic:
have : IsProbabilityMeasure ℙ := isProbabilityMeasure hnt.1 hnt.2 huX
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
neg :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
neg₁ :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume

Tactic:
constructor
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume

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

Premises used: aestronglyMeasurable_id, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume

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

Premises used: AEMeasurable.aestronglyMeasurable, Measurable.aemeasurable, MeasureTheory.measurable_pdf, aestronglyMeasurable_id, AEMeasurable.ennreal_toReal, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume

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

Premises used: MeasureTheory.pdf.IsUniform.pdf_eq, IsCompact.measurableSet, MeasureTheory.pdf.hasFiniteIntegral_mul
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
neg :
  ∫⁻ (x : ℝ),
      ‖x‖ₑ * s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1) x ≠
    ∞
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x_1 : ℝ) ↦ x_1 * (pdf X ℙ volume x_1).toReal) volume

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

Premises used: MeasureTheory.pdf.IsUniform.pdf_eq, IsCompact.measurableSet, MeasureTheory.pdf.hasFiniteIntegral_mul
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
neg :
  let ind := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1;
  ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ∞
⊢ ∫⁻ (x : ℝ),
      ‖x‖ₑ * s.indicator (HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1) x ≠
    ∞

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

Premises used: MeasureTheory.MeasureSpace.volume, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1
⊢ ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun (x : ℝ) ↦ ‖x‖ₑ * ind x) 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
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun (x : ℝ) ↦ ‖x‖ₑ * ind x) x
neg : ∫⁻ (x : ℝ) in s, HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ∂volume ≠ ∞
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ∞

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

Premises used: Pi.one_apply, MeasureTheory.lintegral_indicator, smul_eq_mul, mul_one, IsCompact.measurableSet, Pi.smul_apply
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun (x : ℝ) ↦ ‖x‖ₑ * ind x) x
neg : HMul.hMul (β := ℝ≥0∞) (∫⁻ (a : ℝ) in s, ‖a‖ₑ ∂volume) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ≠ ∞
⊢ ∫⁻ (x : ℝ) in s, HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ∂volume ≠ ∞

Tactic:
rw [lintegral_mul_const _ measurable_enorm]

Premises used: MeasureTheory.lintegral_mul_const, measurable_enorm
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun (x : ℝ) ↦ ‖x‖ₑ * ind x) x
⊢ HMul.hMul (β := ℝ≥0∞) (∫⁻ (a : ℝ) in s, ‖a‖ₑ ∂volume) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ≠ ∞

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

Premises used: Iff.mpr, ENNReal.mul_ne_top, And.right, And.left, continuous_nnnorm, ENNReal.inv_lt_top, pos_iff_ne_zero, LT.lt.ne, MeasureTheory.setLIntegral_lt_top_of_isCompact
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt :
  ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := HSMul.hSMul (α := ℝ≥0∞) (β := ℝ → ℝ≥0∞) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun (x : ℝ) ↦ ‖x‖ₑ * ind x) x
⊢ HMul.hMul (β := ℝ≥0∞) (∫⁻ (a : ℝ) in s, ‖a‖ₑ ∂volume) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ≠ ∞

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

Premises used: Iff.mpr, ENNReal.mul_ne_top, And.right, And.left, continuous_nnnorm, ENNReal.inv_lt_top, pos_iff_ne_zero, LT.lt.ne, MeasureTheory.setLIntegral_lt_top_of_isCompact
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : IsUniform X s ℙ volume
rw :
  Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ)
    (∫ (x : ℝ),
      x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s))
⊢ ∫ (x : Ω), X x ∂ℙ =
    ENNReal.toReal ((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (restrict volume s) fun (x : ℝ) ↦ x

Tactic:
rw [← smul_eq_mul, ← integral_smul_measure]

Premises used: smul_eq_mul, MeasureTheory.integral_smul_measure
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
rw :
  Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ)
    (∫ (x : ℝ),
      x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s))

Tactic:
rw [← huX]
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
pos :
  ∀ (hX : AEMeasurable X ℙ),
    Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
neg :
  ∀ (hX : ¬AEMeasurable X ℙ),
    Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)

Tactic:
by_cases hX : AEMeasurable X ℙ

Premises used: AEMeasurable
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
hX : AEMeasurable X ℙ
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)

Tactic:
(integral_map hX aestronglyMeasurable_id).symm

Premises used: MeasureTheory.integral_map, aestronglyMeasurable_id, Eq.symm
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
hX : AEMeasurable X ℙ
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)

Tactic:
exact (integral_map hX aestronglyMeasurable_id).symm

Premises used: MeasureTheory.integral_map, aestronglyMeasurable_id, Eq.symm
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
hX : ¬AEMeasurable X ℙ
neg : ¬AEStronglyMeasurable X ℙ
⊢ Eq (α := ℝ) (∫ (x : Ω), X x ∂ℙ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.map X ℙ) fun (x : ℝ) ↦ x)

Tactic:
rw [map_of_not_aemeasurable hX, integral_zero_measure, integral_non_aestronglyMeasurable]

Premises used: MeasureTheory.integral_non_aestronglyMeasurable, MeasureTheory.integral_zero_measure, MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX :
  Measure.map X ℙ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) (((volume : (a : Set ℝ) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (restrict volume s)
hX neg neg₁ neg₂ neg₃ : ¬AEMeasurable X ℙ
⊢ ¬AEStronglyMeasurable X ℙ

Tactic:
rwa [aestronglyMeasurable_iff_aemeasurable]

Premises used: aestronglyMeasurable_iff_aemeasurable
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
s : Set E
⊢ IsUniform id s μ[|s] μ

Tactic:
map_id

Premises used: MeasureTheory.Measure.map_id, MeasureTheory.pdf.IsUniform
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hs : MeasurableSet s
hu : IsUniform X s ℙ μ
⊢ (fun (x : E) ↦ uniformPDF s x μ) =ᶠ[ae μ] pdf X ℙ μ

Tactic:
(hu.pdf_eq hs).symm.trans (ae_eq_refl _)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.ae_eq_refl, MeasureTheory.pdf.uniformPDF, MeasureTheory.pdf.IsUniform.pdf_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
s : Set E
x : E
⊢ uniformPDF s x μ = if x ∈ s then ((μ : (a : Set E) → ℝ≥0∞) s)⁻¹ else 0

Tactic:
norm_num [uniformPDF, Set.indicator]

Premises used: Set.indicator, MeasureTheory.pdf.uniformPDF
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
refine_1 : Eq (α := ℝ≥0∞) (∑ a ∈ s, (fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 1
refine_2 : ∀ a ∉ s, Eq (α := ℝ≥0∞) ((fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 0
⊢ PMF α

Tactic:
refine ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s ?_ ?_

Premises used: Membership.mem, PMF.ofFinset, Nat.cast, Inv.inv, Finset.card, OfNat.ofNat, ite
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
refine_1 : HMul.hMul (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (↑(#s) : ℝ≥0∞)⁻¹ = 1
⊢ Eq (α := ℝ≥0∞) (∑ a ∈ s, (fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 1

Tactic:
simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]

Premises used: Finset.sum_ite_mem, Finset.inter_self, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ Ne (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) 0

Tactic:
simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using
        Finset.nonempty_iff_ne_empty.1 hs

Premises used: Ne, Finset.nonempty_iff_ne_empty, Nat.cast_eq_zero, Finset.card_eq_zero, Iff.mp
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ Ne (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) 0

Tactic:
have : (s.card : ℝ≥0∞) ≠ 0 := by
      simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using
        Finset.nonempty_iff_ne_empty.1 hs
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
this : Ne (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) 0
⊢ HMul.hMul (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (↑(#s) : ℝ≥0∞)⁻¹ = 1

Tactic:
ENNReal.mul_inv_cancel this <| ENNReal.natCast_ne_top s.card

Premises used: ENNReal.natCast_ne_top, setOf, ENNReal.mul_inv_cancel, Finset.card
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
this : Ne (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) 0
⊢ HMul.hMul (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (↑(#s) : ℝ≥0∞)⁻¹ = 1

Tactic:
exact ENNReal.mul_inv_cancel this <| ENNReal.natCast_ne_top s.card

Premises used: ENNReal.natCast_ne_top, ENNReal.mul_inv_cancel, Finset.card
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
x : α
hx : x ∉ s
⊢ Eq (α := ℝ≥0∞) ((fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) x) 0

Tactic:
simp only [hx, if_false]

Premises used: if_false
-- Module: Mathlib.Probability.Distributions.Uniform
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ∀ a ∉ s, Eq (α := ℝ≥0∞) ((fun (a : α) ↦ (if a ∈ s then (↑(#s) : ℝ≥0∞)⁻¹ else 0 : ℝ≥0∞)) a) 0

Tactic:
exact fun x hx => by simp only [hx, if_false]