awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mE)
    (fun (x : E) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ))
    (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
rw :
  Eq (α := ℝ)
    (∫ (x : E),
      HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) (x - ∫ (x : E), x ∂μ) : ℝ)
        ((L₂ : (a : E) → ℝ) (x - ∫ (x : E), x ∂μ) : ℝ) ∂μ)
    (∫ (x : E),
      HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
        HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ)
h₁ : MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (∫ (x : E),
        HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
          HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ :
      ℝ)

Tactic:
rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply,
    integral_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.covarianceBilinDual, ProbabilityTheory.uncenteredCovarianceBilinDual_apply
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ L : StrongDual ℝ E
⊢ LE.le (α := ℝ≥0∞) 1 2

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ : ℝ) ((L : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ)

Tactic:
have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) :=
      L.integral_comp_comm (h.integrable (by simp))
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
hL :
  ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ : ℝ) ((L : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ)
⊢ Eq (α := ℝ)
    (∫ (x : E),
      HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) (x - ∫ (x : E), x ∂μ) : ℝ)
        ((L₂ : (a : E) → ℝ) (x - ∫ (x : E), x ∂μ) : ℝ) ∂μ)
    (∫ (x : E),
      HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
        HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ)

Tactic:
simp [← hL]
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)

Tactic:
(measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h.sub (memLp_const _)

Premises used: Iff.mpr, MeasurableEmbedding.memLp_map_measure_iff, measurableEmbedding_subRight, MeasureTheory.MemLp.sub, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)

Tactic:
exact (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h.sub (memLp_const _)

Premises used: Iff.mpr, MeasurableEmbedding.memLp_map_measure_iff, measurableEmbedding_subRight, MeasureTheory.MemLp.sub, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
rw :
  Eq (α := ℝ)
    (∫ (x : E),
      HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
        HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ)
    (∫ (x : E),
      HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) (x - ∫ (x : E), id x ∂μ) : ℝ)
        ((L₂ : (a : E) → ℝ) (x - ∫ (x : E), id x ∂μ) : ℝ) ∂μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (∫ (x : E),
        HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) (x - ∫ (x : E), id x ∂μ) : ℝ)
          ((L₂ : (a : E) → ℝ) (x - ∫ (x : E), id x ∂μ) : ℝ) ∂μ :
      ℝ)

Tactic:
rw [covarianceBilinDual_apply h]

Premises used: ProbabilityTheory.covarianceBilinDual_apply
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ : ℝ) ((L : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ)

Tactic:
have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) :=
    L.integral_comp_comm (h.integrable (by simp))
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
hL :
  ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ : ℝ) ((L : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ)
⊢ Eq (α := ℝ)
    (∫ (x : E),
      HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
        HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ)
    (∫ (x : E),
      HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) (x - ∫ (x : E), id x ∂μ) : ℝ)
        ((L₂ : (a : E) → ℝ) (x - ∫ (x : E), id x ∂μ) : ℝ) ∂μ)

Tactic:
simp [← hL]
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
rw :
  ∫ (x : E),
      HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
        HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ =
    cov[(⇑L₁ : (a : E) → ℝ), (⇑L₂ : (a : E) → ℝ); μ]
rw₁ rw₂ :
  Eq (α := ℝ)
    (∫ (x : E),
      HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
        HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ)
    (∫ (ω : E),
      HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) ω : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
        HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) ω : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ)
⊢ (((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      L₂ =
    cov[(⇑L₁ : (a : E) → ℝ), (⇑L₂ : (a : E) → ℝ); μ]

Tactic:
rw [covarianceBilinDual_apply h, covariance]

Premises used: ProbabilityTheory.covarianceBilinDual_apply, ProbabilityTheory.covariance
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : StrongDual ℝ E
⊢ AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : StrongDual ℝ E
rw : cov[(⇑L : (a : E) → ℝ), (⇑L : (a : E) → ℝ); μ] = Var[(⇑L : (a : E) → ℝ); μ]
rw₁ rw₂ : Var[(⇑L : (a : E) → ℝ); μ] = Var[(⇑L : (a : E) → ℝ); μ]
⊢ (((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      L =
    Var[(⇑L : (a : E) → ℝ); μ]

Tactic:
rw [covarianceBilinDual_eq_covariance h, covariance_self (by fun_prop)]

Premises used: ProbabilityTheory.covarianceBilinDual_eq_covariance, ProbabilityTheory.covariance_self
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.ae_of_all, MeasureTheory.Integrable.add
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
refine_2 :
  ∀ (ω : Ω),
    ‖rexp (t * X ω)‖ ≤
      ‖HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) (fun (ω : Ω) ↦ rexp (b * X ω)) ω‖
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
refine Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.ae_of_all, MeasureTheory.Integrable.add
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
pos : ∀ (hab : a = b), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
neg : ∀ (hab : ¬a = b), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
by_cases hab : a = b
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
⊢ a = t

Tactic:
have ha_eq_t : a = t := le_antisymm hat (hab ▸ htb)
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
ha_eq_t : a = t
pos : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
rw [← ha_eq_t]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
ha_eq_t : a = t
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ

Tactic:
ha.1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
ha_eq_t : a = t
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ

Tactic:
exact ha.1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
AEMeasurable.aestronglyMeasurable ?_

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
neg : AEMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
refine AEMeasurable.aestronglyMeasurable ?_

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
measurable_exp.comp_aemeasurable (AEMeasurable.const_mul ?_ _)

Premises used: AEMeasurable.const_mul, Real.exp, Real.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
neg : AEMeasurable X μ
⊢ AEMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
refine measurable_exp.comp_aemeasurable (AEMeasurable.const_mul ?_ _)

Premises used: AEMeasurable.const_mul, Real.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
pos : ∀ (ha_zero : a = 0), AEMeasurable X μ
neg : ∀ (ha_zero : ¬a = 0), AEMeasurable X μ
⊢ AEMeasurable X μ

Tactic:
by_cases ha_zero : a = 0
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ AEMeasurable X μ

Tactic:
aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul, And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
pos : b ≠ 0
⊢ AEMeasurable X μ

Tactic:
refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul, And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ ¬0 = b

Tactic:
rw [ha_zero] at hab
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
hab₁ : ¬0 = b
⊢ a = 0

Tactic:
rw [ha_zero] at hab
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬0 = b
ha_zero : a = 0
⊢ b ≠ 0

Tactic:
Ne.symm hab

Premises used: Ne.symm
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬0 = b
ha_zero : a = 0
⊢ b ≠ 0

Tactic:
exact Ne.symm hab

Premises used: Ne.symm
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : ¬a = 0
⊢ AEMeasurable X μ

Tactic:
aemeasurable_of_aemeasurable_exp_mul ha_zero ha.1.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul, And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : ¬a = 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul ha_zero ha.1.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul, And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
refine_2 : rexp (t * X ω) ≤ |rexp (a * X ω) + rexp (b * X ω)|
⊢ ‖rexp (t * X ω)‖ ≤
    ‖HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) (fun (ω : Ω) ↦ rexp (b * X ω)) ω‖

Tactic:
simp only [norm_eq_abs, abs_exp, Pi.add_apply]

Premises used: Pi.add_apply, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
⊢ 0 ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
rw : rexp (a * X ω) + rexp (b * X ω)
| |rexp (a * X ω) + rexp (b * X ω)|

Tactic:
rw [abs_of_nonneg (by positivity)]

Premises used: abs_of_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
refine_2 : rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
⊢ rexp (t * X ω) ≤ |rexp (a * X ω) + rexp (b * X ω)|

Tactic:
conv_rhs => rw [abs_of_nonneg (by positivity)]

Premises used: abs_of_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
refine_2 : ∀ (h : 0 ≤ X ω), rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
refine_2₁ : ∀ (h : X ω ≤ 0), rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
rcases le_total 0 (X ω) with h | h

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : 0 ≤ X ω
⊢ rexp (t * X ω) ≤ rexp (b * X ω)

Tactic:
exp_le_exp.mpr (mul_le_mul_of_nonneg_right htb h)

Premises used: Iff.mpr, mul_le_mul_of_nonneg_right, Real.exp_le_exp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : 0 ≤ X ω
⊢ rexp (b * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
le_add_of_nonneg_left (exp_nonneg _)

Premises used: Real.exp_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : 0 ≤ X ω
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
calc exp (t * X ω)
      _ ≤ exp (b * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonneg_right htb h)
      _ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_left (exp_nonneg _)

Premises used: Iff.mpr, HMul.hMul, Real.exp, mul_le_mul_of_nonneg_right, Real.exp_le_exp, Real.exp_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : X ω ≤ 0
⊢ rexp (t * X ω) ≤ rexp (a * X ω)

Tactic:
exp_le_exp.mpr (mul_le_mul_of_nonpos_right hat h)

Premises used: Iff.mpr, mul_le_mul_of_nonpos_right, Real.exp_le_exp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
hb : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : X ω ≤ 0
⊢ rexp (a * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
le_add_of_nonneg_right (exp_nonneg _)

Premises used: le_add_of_nonneg_right, Real.exp_nonneg