awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
rw : (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ = (rexp (t * ε))⁻¹ * mgf X μ t
⊢ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ = rexp (-t * ε) * mgf X μ t

Tactic:
rw [neg_mul, exp_neg]

Premises used: neg_mul, Real.exp_neg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ = (rexp (t * ε))⁻¹ * mgf X μ t

Tactic:
rfl
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
ε₁ : μ.real {ω : Ω | ε ≤ X ω} = μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)}
ε₂ : μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
ε₃ : (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ = rexp (-t * ε) * mgf X μ t
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t

Tactic:
calc
    μ.real {ω | ε ≤ X ω} = μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} := by
      congr 1 with ω
      simp only [Set.mem_setOf_eq, exp_le_exp]
      exact ⟨fun h => mul_le_mul_of_nonneg_left h ht_pos.le,
        fun h => le_of_mul_le_mul_left h ht_pos⟩
    _ ≤ (exp (t * ε))⁻¹ * μ[fun ω => exp (t * X ω)] := by
      have : exp (t * ε) * μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} ≤
          μ[fun ω => exp (t * X ω)] :=
        mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _
      rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]
    _ = exp (-t * ε) * mgf X μ t := by rw [neg_mul, exp_neg]; rfl

Premises used: HMul.hMul, setOf, MeasureTheory.Measure.real, LE.le, Real.exp, ProbabilityTheory.mgf, Neg.neg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
rw : μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (-t * ε) * mgf X μ t

Tactic:
rw [← neg_neg t, ← mgf_neg, neg_neg, ← neg_mul_neg (-t)]

Premises used: ProbabilityTheory.mgf_neg, neg_neg, neg_mul_neg, Neg.neg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)

Tactic:
Eq.trans_le ?_ (measure_ge_le_exp_mul_mgf (-ε) (neg_nonneg.mpr ht) ?_)

Premises used: Iff.mpr, Eq.trans_le, neg_nonneg, ProbabilityTheory.measure_ge_le_exp_mul_mgf, Neg.neg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
refine_1 : μ.real {ω : Ω | X ω ≤ ε} = μ.real {ω : Ω | -ε ≤ (-X) ω}
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * (-X) ω)) μ
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)

Tactic:
refine Eq.trans_le ?_ (measure_ge_le_exp_mul_mgf (-ε) (neg_nonneg.mpr ht) ?_)

Premises used: Iff.mpr, Eq.trans_le, neg_nonneg, ProbabilityTheory.measure_ge_le_exp_mul_mgf, Neg.neg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | X ω ≤ ε} = μ.real {ω : Ω | -ε ≤ (-X) ω}

Tactic:
simp only [Pi.neg_apply, neg_le_neg_iff]

Premises used: Pi.neg_apply, neg_le_neg_iff
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * (-X) ω)) μ

Tactic:
simp_rw [Pi.neg_apply, neg_mul_neg]

Premises used: neg_mul_neg, Pi.neg_apply
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
h_int
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
exact h_int
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε + cgf X μ t)

Tactic:
(measure_ge_le_exp_mul_mgf ε ht h_int).trans ?_

Premises used: ProbabilityTheory.measure_ge_le_exp_mul_mgf, LE.le.trans
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
refine : rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε + cgf X μ t)

Tactic:
refine (measure_ge_le_exp_mul_mgf ε ht h_int).trans ?_

Premises used: ProbabilityTheory.measure_ge_le_exp_mul_mgf, LE.le.trans
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
rw : rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)

Tactic:
rw [exp_add]

Premises used: Real.exp_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)

Tactic:
mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

Premises used: ProbabilityTheory.mgf_nonneg, le_rfl, Real.le_exp_log, LT.lt.le, mul_le_mul, Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)

Tactic:
exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

Premises used: ProbabilityTheory.mgf_nonneg, le_rfl, Real.le_exp_log, LT.lt.le, mul_le_mul, Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (-t * ε + cgf X μ t)

Tactic:
(measure_le_le_exp_mul_mgf ε ht h_int).trans ?_

Premises used: ProbabilityTheory.measure_le_le_exp_mul_mgf, LE.le.trans
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
refine : rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
⊢ μ.real {ω : Ω | X ω ≤ ε} ≤ rexp (-t * ε + cgf X μ t)

Tactic:
refine (measure_le_le_exp_mul_mgf ε ht h_int).trans ?_

Premises used: ProbabilityTheory.measure_le_le_exp_mul_mgf, LE.le.trans
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
rw : rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)

Tactic:
rw [exp_add]

Premises used: Real.exp_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)

Tactic:
mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

Premises used: ProbabilityTheory.mgf_nonneg, le_rfl, Real.le_exp_log, LT.lt.le, mul_le_mul, Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)

Tactic:
exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

Premises used: ProbabilityTheory.mgf_nonneg, le_rfl, Real.le_exp_log, LT.lt.le, mul_le_mul, Real.exp_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
rw : IsProbabilityMeasure (m0 := measurableSpace) (Measure.dirac x)
⊢ IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)

Tactic:
rw [hX]
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
⊢ IsProbabilityMeasure (m0 := measurableSpace) (Measure.dirac x)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
⊢ IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)

Tactic:
have : IsProbabilityMeasure (μ.map X) := by rw [hX]; infer_instance
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Eq (α := Measure ℝ) (Measure.map X μ) (Measure.dirac x)
t : ℝ
this : IsProbabilityMeasure (m0 := measurableSpace) (Measure.map X μ)
rw : mgf (m := measurableSpace) id (Measure.map X μ) t = rexp (x * t)
rw₁ :
  (@integral _ _ _ _ measurableSpace (Measure.map X μ) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
rw₂ :
  (@integral _ _ _ _ measurableSpace (Measure.dirac x) fun (x : ℝ) ↦ (fun (ω : ℝ) ↦ rexp (t * id ω)) x) = rexp (x * t)
rw₃ : rexp (t * id x) = rexp (x * t)
rw₄ : rexp (id x * t) = rexp (x * t)
rw₅ rw₆ : rexp (x * t) = rexp (x * t)
⊢ mgf X μ t = rexp (x * t)

Tactic:
rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
    mul_comm, id_def]

Premises used: AEMeasurable.of_map_ne_zero, id_def, MeasureTheory.integral_dirac, MeasureTheory.IsProbabilityMeasure.ne_zero, mul_comm, ProbabilityTheory.mgf_id_map, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
inst : MeasurableSingletonClass Ω
ω : Ω
rw : (@integral _ _ _ _ m (Measure.dirac ω) fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * X ω)) x) = rexp (t * X ω)
rw₁ rw₂ : rexp (t * X ω) = rexp (t * X ω)
⊢ mgf (m := m) X (Measure.dirac ω) t = rexp (t * X ω)

Tactic:
rw [mgf, integral_dirac]

Premises used: MeasureTheory.integral_dirac, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
(measurable_exp.comp_aemeasurable (hX.const_mul t)).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.const_mul, Real.exp, Real.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
.of_mem_Icc 0 (rexp (t * b)) (measurable_exp.comp_aemeasurable (hX.const_mul t)) ?_

Premises used: HMul.hMul, AEMeasurable.const_mul, Real.exp, Real.measurable_exp, MeasureTheory.Integrable.of_mem_Icc, Measurable.comp_aemeasurable, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
refine : ∀ᵐ (ω : Ω) ∂μ, rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
refine .of_mem_Icc 0 (rexp (t * b)) (measurable_exp.comp_aemeasurable (hX.const_mul t)) ?_
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
h : ∀ (ω : Ω) (hb : X ω ≤ b), rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))
⊢ ∀ᵐ (ω : Ω) ∂μ, rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))

Tactic:
filter_upwards [hb] with ω hb
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb_1 : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
hb : X ω ≤ b
⊢ 0 ≤ rexp (t * X ω)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb_1 : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
hb : X ω ≤ b
a : 0 ≤ t
⊢ rexp (t * X ω) ≤ rexp (t * b)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb_1 : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
hb : X ω ≤ b
⊢ rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))

Tactic:
exact ⟨by positivity, by gcongr⟩
-- Module: Mathlib.Probability.Moments.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
h : Integrable id μ
L : E →L[𝕜] F
change : Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) (id x) ∂μ : F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F)
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) x ∂μ : F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F)

Tactic:
change ∫ x, L (id x) ∂μ = _
-- Module: Mathlib.Probability.Moments.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
h : Integrable id μ
L : E →L[𝕜] F
rw rw₁ : Eq.{u_3 + 1} (α := F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F)
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) (id x) ∂μ : F) ((L : (a : E) → F) (∫ (x : E), id x ∂μ) : F)

Tactic:
rw [L.integral_comp_comm h]

Premises used: ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.Probability.Moments.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
h : Integrable id μ
L : E →L[𝕜] F
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) x ∂μ : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)

Tactic:
L.integral_comp_id_comm' h

Premises used: ContinuousLinearMap.integral_comp_id_comm'
-- Module: Mathlib.Probability.Moments.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : OpensMeasurableSpace E
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
inst_13 : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : OpensMeasurableSpace E
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
inst_13 : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ AEStronglyMeasurable (β := F) (m₀ := inst_11) (fun (x : F) ↦ x) (Measure.map (⇑L : (a : E) → F) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : OpensMeasurableSpace E
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
inst_13 : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
rw : Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) x ∂μ : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)
⊢ Eq.{u_3 + 1} (α := F) (@integral _ _ _ _ inst_11 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ x : F)
    ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)

Tactic:
rw [integral_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Moments.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : OpensMeasurableSpace E
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
inst_13 : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ Eq.{u_3 + 1} (α := F) (∫ (x : E), (L : (a : E) → F) x ∂μ : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)

Tactic:
simp [L.integral_comp_id_comm h]

Premises used: ContinuousLinearMap.integral_comp_id_comm
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (z.re * X ω)) μ
rw : ¬Integrable (ε := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ
⊢ complexMGF X μ z = 0

Tactic:
rw [complexMGF, integral_undef]

Premises used: MeasureTheory.integral_undef, ProbabilityTheory.complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (z.re * X ω)) μ
⊢ AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (z.re * X ω)) μ
rw : ¬Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖cexp (z * (↑(X a) : ℂ))‖) μ
⊢ ¬Integrable (ε := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
rw [← integrable_norm_iff (by fun_prop)]

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (z.re * X ω)) μ
⊢ ¬Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖cexp (z * (↑(X a) : ℂ))‖) μ

Tactic:
simpa [Complex.norm_exp] using h

Premises used: Complex.norm_exp
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
h : ∀ (t : ℂ), complexMGF (m := Real.measurableSpace) id (Measure.map X μ) t = complexMGF X μ t
⊢ complexMGF (m := Real.measurableSpace) id (Measure.map X μ) = complexMGF X μ

Tactic:
ext t
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
h : ∫ (x : Ω), cexp (t * (↑(id (X x)) : ℂ)) ∂μ = complexMGF X μ t
h₁ :
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (ω : ℝ) ↦ cexp (t * (↑(id ω) : ℂ))) (Measure.map X μ)
⊢ complexMGF (m := Real.measurableSpace) id (Measure.map X μ) t = complexMGF X μ t

Tactic:
rw [complexMGF, integral_map hX]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ ∫ (x : Ω), cexp (t * (↑(id (X x)) : ℂ)) ∂μ = complexMGF X μ t

Tactic:
rfl
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (ω : ℝ) ↦ cexp (t * (↑(id ω) : ℂ))) (Measure.map X μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
rw : complexMGF (m := Real.measurableSpace) id (Measure.map X μ) = complexMGF Y μ'
rw₁ :
  complexMGF (m := Real.measurableSpace) id (Measure.map X μ) =
    complexMGF (m := Real.measurableSpace) id (Measure.map Y μ')
rw₂ rw₃ :
  complexMGF (m := Real.measurableSpace) id (Measure.map Y μ') =
    complexMGF (m := Real.measurableSpace) id (Measure.map Y μ')
⊢ complexMGF X μ = complexMGF Y μ'

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

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.complexMGF_id_map, ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
rw :
  Norm.norm (E := ℂ) (∫ (ω : Ω), cexp (((↑z.re : ℂ) + (↑z.im : ℂ) * I) * (↑(X ω) : ℂ)) ∂μ) ≤
    mgf X μ ((↑z.re : ℂ) + (↑z.im : ℂ) * I).re
⊢ ‖complexMGF X μ z‖ ≤ mgf X μ z.re

Tactic:
rw [complexMGF, ← re_add_im z]

Premises used: Complex.re_add_im, ProbabilityTheory.complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
simp_rw :
  Norm.norm (E := ℂ) (∫ (ω : Ω), cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ)) ∂μ) ≤
    mgf X μ z.re
⊢ Norm.norm (E := ℂ) (∫ (ω : Ω), cexp (((↑z.re : ℂ) + (↑z.im : ℂ) * I) * (↑(X ω) : ℂ)) ∂μ) ≤
    mgf X μ ((↑z.re : ℂ) + (↑z.im : ℂ) * I).re

Tactic:
simp_rw [add_mul, Complex.exp_add, re_add_im]

Premises used: add_mul, Complex.exp_add, Complex.re_add_im
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ Norm.norm (E := ℂ) (∫ (ω : Ω), cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ)) ∂μ) ≤
    ∫ (ω : Ω), ‖cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ))‖ ∂μ

Tactic:
norm_integral_le_integral_norm _

Premises used: MeasureTheory.norm_integral_le_integral_norm