awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hX : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ mgf X μ t = 0

Tactic:
simp only [mgf, integral_undef hX]

Premises used: MeasureTheory.integral_undef, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hX : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ cgf X μ t = 0

Tactic:
simp only [cgf, mgf_undef hX, log_zero]

Premises used: ProbabilityTheory.cgf, Real.log_zero, ProbabilityTheory.mgf_undef
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)

Tactic:
simp only [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)

Tactic:
have : ∫ x : Ω, exp (t * X x) ∂μ = ∫ x : Ω in Set.univ, exp (t * X x) ∂μ := by
    simp only [Measure.restrict_univ]
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) ∩ Set.univ) : ℝ≥0∞)
rw₁ : (ae (μ.restrict Set.univ)).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ rexp (t * X x)
rw₂ : IntegrableOn (ε := ℝ) (fun (x : Ω) ↦ rexp (t * X x)) Set.univ μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : Ω), rexp (t * X x) ∂μ)

Tactic:
rw [this, setIntegral_pos_iff_support_of_nonneg_ae _ _]

Premises used: MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) x ↔
      Membership.mem (γ := Set Ω) Set.univ x
⊢ Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ

Tactic:
ext1 x
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
x : Ω
h : rexp (t * X x) ≠ 0
⊢ Membership.mem (γ := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) x ↔
    Membership.mem (γ := Set Ω) Set.univ x

Tactic:
simp only [Function.mem_support, Set.mem_univ, iff_true]

Premises used: iff_true, Set.mem_univ, Function.mem_support
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
x : Ω
⊢ rexp (t * X x) ≠ 0

Tactic:
(exp_pos _).ne'

Premises used: LT.lt.ne', Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
x : Ω
⊢ rexp (t * X x) ≠ 0

Tactic:
exact (exp_pos _).ne'

Premises used: LT.lt.ne', Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
⊢ Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ

Tactic:
have h_eq_univ : (Function.support fun x : Ω => exp (t * X x)) = Set.univ := by
      ext1 x
      simp only [Function.mem_support, Set.mem_univ, iff_true]
      exact (exp_pos _).ne'
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
h_eq_univ : Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ
rw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) ∩ Set.univ) : ℝ≥0∞)

Tactic:
rw [h_eq_univ, Set.inter_univ _]

Premises used: Set.inter_univ
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
h_eq_univ : Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
Ne.bot_lt ?_

Premises used: Ne.bot_lt
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
h_eq_univ : Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ
refine : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (⊥ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
refine Ne.bot_lt ?_

Premises used: Ne.bot_lt
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
h_eq_univ : Eq.{u_1 + 1} (α := Set Ω) (Function.support (M := ℝ) fun (x : Ω) ↦ rexp (t * X x)) Set.univ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (⊥ : ℝ≥0∞)

Tactic:
simp only [hμ, ENNReal.bot_eq_zero, Ne, Measure.measure_univ_eq_zero, not_false_iff]

Premises used: ENNReal.bot_eq_zero, Ne, MeasureTheory.Measure.measure_univ_eq_zero, not_false_iff
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
h : ∀ (x : Ω), 0 x ≤ rexp (t * X x)
⊢ (ae (μ.restrict Set.univ)).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ rexp (t * X x)

Tactic:
filter_upwards with x
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
x : Ω
⊢ 0 ≤ rexp (t * X x)

Tactic:
(exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
x : Ω
⊢ 0 ≤ rexp (t * X x)

Tactic:
exact (exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
this : Eq (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ)
rwa rwa₁ rwa₂ rwa₃ : Integrable (ε := ℝ) (fun (x : Ω) ↦ rexp (t * X x)) μ
⊢ IntegrableOn (ε := ℝ) (fun (x : Ω) ↦ rexp (t * X x)) Set.univ μ

Tactic:
rwa [integrableOn_univ]

Premises used: MeasureTheory.integrableOn_univ
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsProbabilityMeasure μ
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ 0 < mgf X μ t

Tactic:
mgf_pos' (IsProbabilityMeasure.ne_zero μ) h_int_X

Premises used: ProbabilityTheory.mgf_pos', MeasureTheory.IsProbabilityMeasure.ne_zero
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
⊢ 0 < mgf X μ t ↔ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
⟨fun h ↦ ?_, fun h ↦ mgf_pos' hμ.out h⟩

Premises used: ProbabilityTheory.mgf_pos', Iff.intro, NeZero.out
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
refine : ∀ (h : 0 < mgf X μ t), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ 0 < mgf X μ t ↔ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ mgf_pos' hμ.out h⟩
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
h : 0 < mgf X μ t
contrapose! : ∀ (h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ), mgf X μ t ≤ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
contrapose! h with h
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ mgf X μ t ≤ 0

Tactic:
simp [mgf_undef h]

Premises used: ProbabilityTheory.mgf_undef
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : NeZero μ
hX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
rw : rexp (log (mgf X μ t)) = mgf X μ t
rw₁ rw₂ : mgf X μ t = mgf X μ t
⊢ rexp (cgf X μ t) = mgf X μ t

Tactic:
rw [cgf, exp_log (mgf_pos' hμ.out hX)]

Premises used: ProbabilityTheory.cgf, Real.exp_log, ProbabilityTheory.mgf_pos', NeZero.out
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
t : ℝ
hX : AEStronglyMeasurable (β := ℝ) (m₀ := m) (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y μ)
simp_rw :
  Eq (α := ℝ) (@integral _ _ _ _ m (Measure.map Y μ) fun (x : Ω) ↦ rexp (t * X x)) (∫ (x : Ω'), rexp (t * (X ∘ Y) x) ∂μ)
simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω'), rexp (t * X (Y x)) ∂μ) (∫ (x : Ω'), rexp (t * (X ∘ Y) x) ∂μ)
⊢ mgf (m := m) X (Measure.map Y μ) t = mgf (X ∘ Y) μ t

Tactic:
simp_rw [mgf, integral_map hY hX, Function.comp_apply]

Premises used: MeasureTheory.integral_map, Function.comp_apply, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
h : ∀ (t : ℝ), mgf (m := measurableSpace) id (Measure.map X μ) t = mgf X μ t
⊢ mgf (m := measurableSpace) id (Measure.map X μ) = mgf X μ

Tactic:
ext t
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
h : AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)
⊢ mgf (m := measurableSpace) id (Measure.map X μ) t = mgf X μ t

Tactic:
rw [mgf_map hX, Function.id_comp]

Premises used: ProbabilityTheory.mgf_map, Function.id_comp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)

Tactic:
(measurable_const_mul _).exp.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, MeasurableMul.measurable_const_mul, Measurable.exp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)

Tactic:
exact (measurable_const_mul _).exp.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, MeasurableMul.measurable_const_mul, Measurable.exp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
rw rw₁ : rexp (t * Y ω) = rexp (t * Y ω)
⊢ rexp (t * X ω) = rexp (t * Y ω)

Tactic:
rw [hω]
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
h : X =ᶠ[ae μ] Y
h₁ :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦ Eq (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * X ω)) x) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x)) x}
            x}
      a
h₂ h₃ : ∀ (ω : Ω) (hω : X ω = Y ω), rexp (t * X ω) = rexp (t * Y ω)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)

Tactic:
filter_upwards [h] with ω hω using by rw [hω]
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
rw : mgf (m := measurableSpace) id (Measure.map X μ) = mgf Y μ'
rw₁ : mgf (m := measurableSpace) id (Measure.map X μ) = mgf (m := measurableSpace) id (Measure.map Y μ')
rw₂ rw₃ : mgf (m := measurableSpace) id (Measure.map Y μ') = mgf (m := measurableSpace) id (Measure.map Y μ')
⊢ mgf X μ = mgf Y μ'

Tactic:
rw [← mgf_id_map h.aemeasurable_fst, ← mgf_id_map h.aemeasurable_snd, h.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.mgf_id_map, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (-X) x) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * -X x) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
simp_rw₂ : Eq (α := ℝ) (∫ (x : Ω), rexp (-(t * X x)) ∂μ) (∫ (x : Ω), rexp (-t * X x) ∂μ)
⊢ mgf (-X) μ t = mgf X μ (-t)

Tactic:
simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul]

Premises used: neg_mul, ProbabilityTheory.mgf, Pi.neg_apply, mul_neg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
simp_rw : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α • X) x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
simp_rw₁ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * α • X x) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
simp_rw₂ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α * X x)) ∂μ) (∫ (x : Ω), rexp (α * t * X x) ∂μ)
simp_rw₃ : Eq (α := ℝ) (∫ (x : Ω), rexp (t * (α * X x)) ∂μ) (∫ (x : Ω), rexp (t * α * X x) ∂μ)
⊢ mgf (α • X) μ t = mgf X μ (α * t)

Tactic:
simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]

Premises used: mul_assoc, mul_comm, smul_eq_mul, ProbabilityTheory.mgf, Pi.smul_apply
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun (ω : Ω) ↦ α * X ω) μ t = mgf X μ (α * t)

Tactic:
mgf_smul_left α

Premises used: ProbabilityTheory.mgf_smul_left
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
rw : Eq (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * (α + X ω))) x ∂μ) (∫ (a : Ω), rexp (t * α) * rexp (t * X a) ∂μ)
⊢ mgf (fun (ω : Ω) ↦ α + X ω) μ t = rexp (t * α) * mgf X μ t

Tactic:
rw [mgf, mgf, ← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
e_f : ∀ (x : Ω), (fun (ω : Ω) ↦ rexp (t * (α + X ω))) x = rexp (t * α) * rexp (t * X x)
⊢ Eq (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * (α + X ω))) x ∂μ) (∫ (a : Ω), rexp (t * α) * rexp (t * X a) ∂μ)

Tactic:
congr with x
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
e_f : rexp (t * α + t * X x) = rexp (t * α) * rexp (t * X x)
e_f₁ e_f₂ : rexp (t * α) * rexp (t * X x) = rexp (t * α) * rexp (t * X x)
⊢ rexp (t * (α + X x)) = rexp (t * α) * rexp (t * X x)

Tactic:
rw [mul_add, exp_add]

Premises used: mul_add, Real.exp_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun (ω : Ω) ↦ X ω + α) μ t = mgf X μ t * rexp (t * α)

Tactic:
simp only [add_comm, mgf_const_add, mul_comm]

Premises used: ProbabilityTheory.mgf_const_add, add_comm, mul_comm
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ν : Measure Ω
hμ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hν : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) ν
rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂(μ + ν) = mgf X μ t + mgf X ν t
rw₁ : HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) = mgf X μ t + mgf X ν t
rw₂ :
  HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) =
    ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ + mgf X ν t
rw₃ rw₄ :
  HAdd.hAdd (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * X x) ∂ν) =
    HAdd.hAdd (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂ν)
⊢ mgf X (μ + ν) t = mgf X μ t + mgf X ν t

Tactic:
rw [mgf, integral_add_measure hμ hν, mgf, mgf]

Premises used: MeasureTheory.integral_add_measure, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
c : ℝ≥0∞
rw : ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂c • μ = c.toReal * mgf X μ t
rw₁ : HSMul.hSMul (β := ℝ) c.toReal (∫ (x : Ω), rexp (t * X x) ∂μ) = c.toReal * mgf X μ t
rw₂ :
  HSMul.hSMul (β := ℝ) c.toReal (∫ (x : Ω), rexp (t * X x) ∂μ) =
    c.toReal * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
rw₃ rw₄ : c.toReal * ∫ (x : Ω), rexp (t * X x) ∂μ = c.toReal * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
⊢ mgf X (c • μ) t = c.toReal * mgf X μ t

Tactic:
rw [mgf, integral_smul_measure, mgf, smul_eq_mul]

Premises used: smul_eq_mul, ProbabilityTheory.mgf, MeasureTheory.integral_smul_measure
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
pos : ∀ (htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ), mgf X μ t ≤ mgf Y μ t
neg : ∀ (htX : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ), mgf X μ t ≤ mgf Y μ t
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
by_cases htX : Integrable (fun ω ↦ exp (t * X ω)) μ

Premises used: HMul.hMul, MeasureTheory.Integrable, Real.exp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
integral_mono_ae htX htY ?_

Premises used: MeasureTheory.integral_mono_ae, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
pos : (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
refine integral_mono_ae htX htY ?_

Premises used: MeasureTheory.integral_mono_ae
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ω : Ω
hω : X ω ≤ Y ω
a : 0 ≤ t
⊢ rexp (t * X ω) ≤ rexp (t * Y ω)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x ≤ Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦ LE.le (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * X ω)) x) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x)) x}
            x}
      a
h₁ h₂ : ∀ (ω : Ω) (hω : X ω ≤ Y ω), rexp (t * X ω) ≤ rexp (t * Y ω)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)

Tactic:
filter_upwards [hXY] with ω hω using by gcongr
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
neg : 0 ≤ mgf Y μ t
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
rw [mgf_undef htX]

Premises used: ProbabilityTheory.mgf_undef
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ 0 ≤ mgf Y μ t

Tactic:
mgf_nonneg

Premises used: ProbabilityTheory.mgf_nonneg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ 0 ≤ mgf Y μ t

Tactic:
exact mgf_nonneg

Premises used: ProbabilityTheory.mgf_nonneg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
pos : ∀ (htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ), mgf Y μ t ≤ mgf X μ t
neg : ∀ (htY : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ), mgf Y μ t ≤ mgf X μ t
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
by_cases htY : Integrable (fun ω ↦ exp (t * Y ω)) μ

Premises used: HMul.hMul, MeasureTheory.Integrable, Real.exp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
integral_mono_ae htY htX ?_

Premises used: MeasureTheory.integral_mono_ae, ProbabilityTheory.mgf