-- Mathlib/Probability/Moments/Basic.lean
theorem measure_ge_le_exp_mul_mgf [IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t)
    (h_int : Integrable (fun ω => exp (t * X ω)) μ) :
    (μ {ω | ε ≤ X ω}).toReal ≤ exp (-t * ε) * mgf X μ t

Proof state:
case inl.hb
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ Set.univ ≠ ⊤

case inl.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ {ω | ε ≤ X ω} ⊆ Set.univ

Tactic:
exacts [measure_ne_top _ _, Set.subset_univ _]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
this : rexp (t * ε) * (μ {ω | rexp (t * ε) ≤ rexp (t * X ω)}).toReal ≤ ∫ (x : Ω), (fun ω => rexp (t * X ω)) x ∂μ
⊢ (μ {ω | rexp (t * ε) ≤ rexp (t * X ω)}).toReal ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun ω => rexp (t * X ω)) x ∂μ

Tactic:
rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε) * mgf X μ t

Tactic:
rcases ht.eq_or_lt with ht_zero_eq | ht_pos

Result:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε) * mgf X μ t

case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε) * mgf X μ t

Proof state:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ rexp (-0 * ε) * mgf X μ 0

Tactic:
simp only [neg_zero, zero_mul, exp_zero, mgf_zero', one_mul]

Result:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ (μ Set.univ).toReal

Proof state:
case e_a.h.e_6.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
ω : Ω
⊢ ε ≤ X ω ↔ t * ε ≤ t * X ω

Tactic:
exact ⟨fun h => mul_le_mul_of_nonneg_left h ht_pos.le,
  fun h => le_of_mul_le_mul_left h ht_pos⟩

Result:
no goals

Proof state:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε) * mgf X μ t

Tactic:
calc
  (μ {ω | ε ≤ X ω}).toReal = (μ {ω | exp (t * ε) ≤ exp (t * X ω)}).toReal := by
    congr with ω
    simp only [Set.mem_setOf_eq, exp_le_exp, gt_iff_lt]
    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 * ε) * (μ {ω | exp (t * ε) ≤ exp (t * X ω)}).toReal ≤
        μ[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

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ (μ {ω | ε ≤ X ω}).toReal = (μ {ω | rexp (t * ε) ≤ rexp (t * X ω)}).toReal

Tactic:
congr with ω

Result:
case e_a.h.e_6.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
ω : Ω
⊢ ω ∈ {ω | ε ≤ X ω} ↔ ω ∈ {ω | rexp (t * ε) ≤ rexp (t * X ω)}

Proof state:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε) * mgf X μ t

Tactic:
rw [ht_zero_eq.symm]

Result:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ rexp (-0 * ε) * mgf X μ 0

Proof state:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ (μ Set.univ).toReal

Tactic:
gcongr

Result:
case inl.hb
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ Set.univ ≠ ⊤

case inl.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ {ω | ε ≤ X ω} ⊆ Set.univ

Proof state:
case e_a.h.e_6.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
ω : Ω
⊢ ω ∈ {ω | ε ≤ X ω} ↔ ω ∈ {ω | rexp (t * ε) ≤ rexp (t * X ω)}

Tactic:
simp only [Set.mem_setOf_eq, exp_le_exp, gt_iff_lt]

Result:
case e_a.h.e_6.h.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
ω : Ω
⊢ ε ≤ X ω ↔ t * ε ≤ t * X ω

Proof state:
Ω : 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

Result:
no goals

Proof state:
Ω : 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:
rw [neg_mul, exp_neg]

Result:
Ω : 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

Proof state:
Ω : 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 * ε) ≤ rexp (t * X ω)}).toReal ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun ω => rexp (t * X ω)) x ∂μ

Tactic:
have : exp (t * ε) * (μ {ω | exp (t * ε) ≤ exp (t * X ω)}).toReal ≤
    μ[fun ω => exp (t * X ω)] :=
  mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
ht_pos : 0 < t
this : rexp (t * ε) * (μ {ω | rexp (t * ε) ≤ rexp (t * X ω)}).toReal ≤ ∫ (x : Ω), (fun ω => rexp (t * X ω)) x ∂μ
⊢ (μ {ω | rexp (t * ε) ≤ rexp (t * X ω)}).toReal ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun ω => rexp (t * X ω)) x ∂μ