awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ∂μ : ℝ) ∂μ)
⊢ 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 ∂μ : ℝ) ∂μ :
      ℝ)
have h₁ : MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
Tactic: rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply,
    integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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
⊢ 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 ∂μ : ℝ) ∂μ)
have hL : ∀ (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))
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ 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 ∂μ) : ℝ) ∂μ :
      ℝ)
have 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 ∂μ) : ℝ) ∂μ)
Tactic: rw [covarianceBilinDual_apply h]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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
⊢ 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 ∂μ) : ℝ) ∂μ)
have hL : ∀ (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))
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ (((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      L₂ =
    cov[(⇑L₁ : (a : E) → ℝ), (⇑L₂ : (a : E) → ℝ); μ]
have 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) → ℝ); μ]
Tactic: rw [covarianceBilinDual_apply h, covariance]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) → ℝ); μ]
⊢ (((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      L₂ =
    cov[(⇑L₁ : (a : E) → ℝ), (⇑L₂ : (a : E) → ℝ); μ]
have 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 ∂μ : ℝ) ∂μ)
Tactic: rw [covarianceBilinDual_apply h, covariance]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ (((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      L =
    Var[(⇑L : (a : E) → ℝ); μ]
have rw : cov[(⇑L : (a : E) → ℝ), (⇑L : (a : E) → ℝ); μ] = Var[(⇑L : (a : E) → ℝ); μ]
Tactic: rw [covarianceBilinDual_eq_covariance h, covariance_self (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) → ℝ); μ]
⊢ (((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      L =
    Var[(⇑L : (a : E) → ℝ); μ]
have rw₁ : Var[(⇑L : (a : E) → ℝ); μ] = Var[(⇑L : (a : E) → ℝ); μ]
Tactic: rw [covarianceBilinDual_eq_covariance h, covariance_self (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 ω)) μ
have refine_1 : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
Tactic: refine Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have refine_2 : ∀ (ω : Ω),
  ‖rexp (t * X ω)‖ ≤
    ‖HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) (fun (ω : Ω) ↦ rexp (b * X ω)) ω‖
Tactic: refine Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have pos : ∀ (hab : a = b), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have neg : ∀ (hab : ¬a = b), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
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 ω)) μ
have ha_eq_t : a = t
Tactic: have ha_eq_t : a = t := le_antisymm hat (hab ▸ htb)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 (t * X ω)) μ
have pos : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) μ
Tactic: rw [← ha_eq_t]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 ω)) μ
have neg : AEMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
Tactic: refine AEMeasurable.aestronglyMeasurable ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 ω)) μ
have neg : AEMeasurable X μ
Tactic: refine measurable_exp.comp_aemeasurable (AEMeasurable.const_mul ?_ _)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 X μ
have pos : ∀ (ha_zero : a = 0), AEMeasurable X μ
Tactic: by_cases ha_zero : a = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 μ
⊢ AEMeasurable X μ
have neg : ∀ (ha_zero : ¬a = 0), AEMeasurable X μ
Tactic: by_cases ha_zero : a = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 μ
have pos : b ≠ 0
Tactic: refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
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
⊢ b ≠ 0
have hab₁ : ¬0 = b
Tactic: rw [ha_zero] at hab
Cleared hypotheses: hab, ha_zero
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
ω : Ω
⊢ ‖rexp (t * X ω)‖ ≤
    ‖HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ rexp (a * X ω)) (fun (ω : Ω) ↦ rexp (b * X ω)) ω‖
have refine_2 : rexp (t * X ω) ≤ |rexp (a * X ω) + rexp (b * X ω)|
Tactic: simp only [norm_eq_abs, abs_exp, Pi.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
ω : Ω
| |rexp (a * X ω) + rexp (b * X ω)|
have rw : rexp (a * X ω) + rexp (b * X ω)
Tactic: rw [abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
ω : Ω
⊢ rexp (t * X ω) ≤ |rexp (a * X ω) + rexp (b * X ω)|
have refine_2 : rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
Tactic: conv_rhs => rw [abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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
ω : Ω
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
have refine_2 : ∀ (h : 0 ≤ X ω), rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
Tactic: rcases le_total 0 (X ω) with h | h
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
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 ω)
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
have refine_2₁ : ∀ (h : X ω ≤ 0), rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
Tactic: rcases le_total 0 (X ω) with h | h
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
Tactic: refine integrable_exp_mul_of_le_of_le (a := -|u|) (b := |u|) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
Tactic: refine integrable_exp_mul_of_le_of_le (a := -|u|) (b := |u|) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have refine_3 : -|u| ≤ t
Tactic: refine integrable_exp_mul_of_le_of_le (a := -|u|) (b := |u|) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
refine_3 : -|u| ≤ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
have refine_4 : t ≤ |u|
Tactic: refine integrable_exp_mul_of_le_of_le (a := -|u|) (b := |u|) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
have refine_1 : ∀ (hu : 0 ≤ u), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
Tactic: rcases le_total 0 u with hu | hu
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
refine_1 : ∀ (hu : 0 ≤ u), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
have refine_1₁ : ∀ (hu : u ≤ 0), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
Tactic: rcases le_total 0 u with hu | hu
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
have refine_2 : ∀ (hu : 0 ≤ u), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
Tactic: rcases le_total 0 u with hu | hu
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
refine_2 : ∀ (hu : 0 ≤ u), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
have refine_2₁ : ∀ (hu : u ≤ 0), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
Tactic: rcases le_total 0 u with hu | hu
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t
have refine_3 : -t ≤ |u|
Tactic: rw [neg_le]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ
have inr : ∀
  (this :
    ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄ (ht₁ : t₁ ∈ integrableExpSet X μ)
      ⦃t₂ : ℝ⦄ (ht₂ : t₂ ∈ integrableExpSet X μ) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (h_le : t₁ ≤ t₂),
      a • t₁ + b • t₂ ∈ integrableExpSet X μ)
  (h_le : t₂ < t₁), a • t₁ + b • t₂ ∈ integrableExpSet X μ
Tactic: wlog! h_le : t₁ ≤ t₂
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inr :
  ∀
    (this :
      ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄ (ht₁ : t₁ ∈ integrableExpSet X μ)
        ⦃t₂ : ℝ⦄ (ht₂ : t₂ ∈ integrableExpSet X μ) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1)
        (h_le : t₁ ≤ t₂), a • t₁ + b • t₂ ∈ integrableExpSet X μ)
    (h_le : t₂ < t₁), a • t₁ + b • t₂ ∈ integrableExpSet X μ
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ
have wlog! : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄ (ht₁ : t₁ ∈ integrableExpSet X μ) ⦃t₂ : ℝ⦄
  (ht₂ : t₂ ∈ integrableExpSet X μ) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (h_le : t₁ ≤ t₂),
  a • t₁ + b • t₂ ∈ integrableExpSet X μ
Tactic: wlog! h_le : t₁ ≤ t₂
Cleared hypotheses: t₁, ht₁, t₂, ht₂, a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄ (ht₁ : t₁ ∈ integrableExpSet X μ)
    ⦃t₂ : ℝ⦄ (ht₂ : t₂ ∈ integrableExpSet X μ) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (h_le : t₁ ≤ t₂),
    a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : t₂ < t₁
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ
have inr : ∀ (hab : b + a = 1)
  (this :
    ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄ (ht₁ : t₁ ∈ integrableExpSet X μ)
      ⦃t₂ : ℝ⦄ (ht₂ : t₂ ∈ integrableExpSet X μ) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (h_le : t₁ ≤ t₂),
      a • t₁ + b • t₂ ∈ integrableExpSet X μ)
  (h_le : t₂ < t₁), b • t₂ + a • t₁ ∈ integrableExpSet X μ
Tactic: rw [add_comm] at hab ⊢
Cleared hypotheses: hab, this, h_le
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ
have refine_1 : t₁ ≤ a • t₁ + b • t₂
Tactic: refine integrable_exp_mul_of_le_of_le ht₁ ht₂ ?_ ?_