awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
rw :
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
have rw₁ : ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), rexp (t * X x) ∂μ ∂μ) =
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ ∂μ)
Tactic: rw [tilted_apply_eq_ofReal_integral _ s, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
have inl : ∀ (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
  ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (a : Ω) ↦ rexp (t * X a - cgf (m := mΩ) X 0 t))
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl :
  ∀ (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
    ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      ENNReal.ofReal (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (a : Ω) ↦ rexp (t * X a - cgf (m := mΩ) X 0 t))
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
have inr : ∀ (hμ : NeZero μ),
  (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
have inr : ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)
Tactic: simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf' hs, exp_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)
have inr : ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
Tactic: rwa [exp_cgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
have inl : ∀ [SFinite.{u_1} (α := Ω) (m0 := mΩ) 0] (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
  ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (a : Ω) ↦ rexp (t * X a - cgf (m := mΩ) X 0 t))
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, inst, ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl :
  ∀ [SFinite.{u_1} (α := Ω) (m0 := mΩ) 0] (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
    ((Measure.tilted 0 fun (x : Ω) ↦ t * X x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
      ENNReal.ofReal (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (a : Ω) ↦ rexp (t * X a - cgf (m := mΩ) X 0 t))
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
have inr : ∀ (hμ : NeZero μ),
  (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
have inr : ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)
Tactic: simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf s, exp_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)
have inr : ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
  ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ)
Tactic: rwa [exp_cgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
  (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
Tactic: rw [setIntegral_tilted' _ _ hs, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
rw :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
    (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
have rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
  (∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) • g x ∂μ)
Tactic: rw [setIntegral_tilted' _ _ hs, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SFinite μ
g : Ω → E
s : Set Ω
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
  (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
Tactic: rw [setIntegral_tilted, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SFinite μ
g : Ω → E
s : Set Ω
rw :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
    (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
have rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
  (∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) • g x ∂μ)
Tactic: rw [setIntegral_tilted, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
have inl : ∀ (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ mΩ (Measure.restrict (Measure.tilted 0 fun (x : Ω) ↦ t * X x) s) fun (x : Ω) ↦ g x)
    (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (x : Ω) ↦ rexp (t * X x - cgf (m := mΩ) X 0 t) • g x)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl :
  ∀ (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
    Eq.{u_2 + 1} (α := E)
      (@integral _ _ _ _ mΩ (Measure.restrict (Measure.tilted 0 fun (x : Ω) ↦ t * X x) s) fun (x : Ω) ↦ g x)
      (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (x : Ω) ↦ rexp (t * X x - cgf (m := mΩ) X 0 t) • g x)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
have inr : ∀ (hμ : NeZero μ),
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
have inr : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
  (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
Tactic: simp_rw [setIntegral_tilted_mul_eq_mgf' _ hs, exp_sub, exp_cgf ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
inr :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
have inr₁ : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
  (∫ (x : Ω) in s, (rexp (t * X x) / rexp (cgf X μ t)) • g x ∂μ)
Tactic: simp_rw [setIntegral_tilted_mul_eq_mgf' _ hs, exp_sub, exp_cgf ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
have inl : ∀ [SFinite.{u_1} (α := Ω) (m0 := mΩ) 0] (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ mΩ (Measure.restrict (Measure.tilted 0 fun (x : Ω) ↦ t * X x) s) fun (x : Ω) ↦ g x)
    (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (x : Ω) ↦ rexp (t * X x - cgf (m := mΩ) X 0 t) • g x)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, inst_2, ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl :
  ∀ [SFinite.{u_1} (α := Ω) (m0 := mΩ) 0] (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
    Eq.{u_2 + 1} (α := E)
      (@integral _ _ _ _ mΩ (Measure.restrict (Measure.tilted 0 fun (x : Ω) ↦ t * X x) s) fun (x : Ω) ↦ g x)
      (@integral _ _ _ _ mΩ (Measure.restrict 0 s) fun (x : Ω) ↦ rexp (t * X x - cgf (m := mΩ) X 0 t) • g x)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
have inr : ∀ (hμ : NeZero μ),
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
have inr : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
  (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
Tactic: simp_rw [setIntegral_tilted_mul_eq_mgf, exp_sub, exp_cgf ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
inr :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, g x ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ)
have inr₁ : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ)
  (∫ (x : Ω) in s, (rexp (t * X x) / rexp (cgf X μ t)) • g x ∂μ)
Tactic: simp_rw [setIntegral_tilted_mul_eq_mgf, exp_sub, exp_cgf ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : Ω), (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
  (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
Tactic: rw [integral_tilted, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
rw :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω), (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
    (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
have rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : Ω), (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ)
  (∫ (ω : Ω), (rexp (t * X ω) / ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) • g ω ∂μ)
Tactic: rw [integral_tilted, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ)
have inl : ∀ (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
  Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ mΩ (Measure.tilted 0 fun (x : Ω) ↦ t * X x) fun (ω : Ω) ↦ g ω)
    (@integral _ _ _ _ mΩ 0 fun (ω : Ω) ↦ rexp (t * X ω - cgf (m := mΩ) X 0 t) • g ω)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl :
  ∀ (ht : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) 0),
    Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ mΩ (Measure.tilted 0 fun (x : Ω) ↦ t * X x) fun (ω : Ω) ↦ g ω)
      (@integral _ _ _ _ mΩ 0 fun (ω : Ω) ↦ rexp (t * X ω - cgf (m := mΩ) X 0 t) • g ω)
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ)
have inr : ∀ (hμ : NeZero μ),
  Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ)
have inr : Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
  (∫ (ω : Ω), (rexp (t * X ω) / rexp (cgf X μ t)) • g ω ∂μ)
Tactic: simp_rw [integral_tilted_mul_eq_mgf, exp_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
    (∫ (ω : Ω), (rexp (t * X ω) / rexp (cgf X μ t)) • g ω ∂μ)
have inr : Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
  (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
Tactic: rwa [exp_cgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (x : Ω), X x ∂μ.tilted fun (x : Ω) ↦ t * X x) = deriv (cgf X μ) t
have simp_rw : Eq (α := ℝ) (∫ (ω : Ω), rexp (t * X ω) / mgf X μ t * X ω ∂μ) (∫ (a : Ω), X a * rexp (t * X a) / mgf X μ t ∂μ)
Tactic: simp_rw [integral_tilted_mul_eq_mgf, deriv_cgf ht, ← integral_div, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ Eq (α := ℝ) (∫ (ω : Ω), rexp (t * X ω) / mgf X μ t * X ω ∂μ) (∫ (a : Ω), X a * rexp (t * X a) / mgf X μ t ∂μ)
have e_f : ∀ (ω : Ω), rexp (t * X ω) / mgf X μ t * X ω = X ω * rexp (t * X ω) / mgf X μ t
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
⊢ MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)
have hX : AEMeasurable X μ
Tactic: have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet ht
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
⊢ MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)
have pos : ∀ (hp : p = 0), MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
pos : ∀ (hp : p = 0), MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)
⊢ MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)
have neg : ∀ (hp : ¬p = 0), MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)
have neg : eLpNorm X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x) < ∞
Tactic: refine ⟨hX.aestronglyMeasurable.mono_ac (tilted_absolutelyContinuous _ _), ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ eLpNorm X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x) < ∞
have neg : (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
neg : (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞
⊢ eLpNorm X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x) < ∞
have neg₁ : (↑p : ℝ≥0∞) ≠ 0
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
neg : (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞
neg₁ : (↑p : ℝ≥0∞) ≠ 0
⊢ eLpNorm X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x) < ∞
have neg₂ : (↑p : ℝ≥0∞) ≠ ∞
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞
have neg : (∫⁻ (a : Ω), ENNReal.ofReal (|X a| ^ (↑p : ℝ)) ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞
Tactic: simp_rw [ENNReal.coe_toReal, ← ofReal_norm, norm_eq_abs,
    ENNReal.ofReal_rpow_of_nonneg (x := |X _|) (p := p) (abs_nonneg (X _)) p.2]