awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
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) ∂μ)
⊢ (μ.tilted fun (x : Ω) ↦ t * X x : (a : Set Ω) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf s, exp_sub]

Premises used: ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf, Real.exp_sub
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst : SFinite μ
s : Set Ω
ht : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hμ : NeZero μ
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 ∂μ)
inr₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
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 ∂μ)
inr₃ inr₄ inr₅ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ 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:
rwa [exp_cgf]

Premises used: ProbabilityTheory.exp_cgf
-- Module: Mathlib.Probability.Moments.Tilted
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 ∂μ)
rw₁ 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 ∂μ)
⊢ 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 ∂μ)

Tactic:
rw [setIntegral_tilted' _ _ hs, mgf]

Premises used: MeasureTheory.setIntegral_tilted', ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Tilted
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 ∂μ)
rw₁ 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 ∂μ)
⊢ 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 ∂μ)

Tactic:
rw [setIntegral_tilted, mgf]

Premises used: MeasureTheory.setIntegral_tilted, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Tilted
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)
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 ∂μ)
⊢ 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μ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
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:
simp
-- Module: Mathlib.Probability.Moments.Tilted
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 ∂μ)
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 ∂μ)
⊢ 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:
simp_rw [setIntegral_tilted_mul_eq_mgf' _ hs, exp_sub, exp_cgf ht]

Premises used: ProbabilityTheory.exp_cgf, ProbabilityTheory.setIntegral_tilted_mul_eq_mgf', Real.exp_sub
-- Module: Mathlib.Probability.Moments.Tilted
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)
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 ∂μ)
⊢ 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μ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
s : Set Ω
inst_2 : 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:
simp
-- Module: Mathlib.Probability.Moments.Tilted
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 ∂μ)
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 ∂μ)
⊢ 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:
simp_rw [setIntegral_tilted_mul_eq_mgf, exp_sub, exp_cgf ht]

Premises used: ProbabilityTheory.exp_cgf, ProbabilityTheory.setIntegral_tilted_mul_eq_mgf, Real.exp_sub
-- Module: Mathlib.Probability.Moments.Tilted
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 ω ∂μ)
rw₁ 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 ω ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)

Tactic:
rw [integral_tilted, mgf]

Premises used: MeasureTheory.integral_tilted, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.Tilted
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 ω)
inr :
  ∀ (hμ : NeZero μ),
    Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
      (∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ)
⊢ 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μ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : Ω → E
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:
simp
-- Module: Mathlib.Probability.Moments.Tilted
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 μ
inr :
  Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
    (∫ (ω : Ω), (rexp (t * X ω) / rexp (cgf X μ t)) • g ω ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), g ω ∂μ.tilted fun (x : Ω) ↦ t * X x)
    (∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ)

Tactic:
simp_rw [integral_tilted_mul_eq_mgf, exp_sub]

Premises used: ProbabilityTheory.integral_tilted_mul_eq_mgf, Real.exp_sub
-- Module: Mathlib.Probability.Moments.Tilted
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 μ
inr :
  Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
    (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
inr₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inr₂ :
  Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
    (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
inr₃ inr₄ inr₅ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ)
    (∫ (ω : Ω), (rexp (t * X ω) / rexp (cgf X μ t)) • g ω ∂μ)

Tactic:
rwa [exp_cgf]

Premises used: ProbabilityTheory.exp_cgf
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
simp_rw : Eq (α := ℝ) (∫ (ω : Ω), rexp (t * X ω) / mgf X μ t * X ω ∂μ) (∫ (a : Ω), X a * rexp (t * X a) / mgf X μ t ∂μ)
⊢ (∫ (x : Ω), X x ∂μ.tilted fun (x : Ω) ↦ t * X x) = deriv (cgf X μ) t

Tactic:
simp_rw [integral_tilted_mul_eq_mgf, deriv_cgf ht, ← integral_div, smul_eq_mul]

Premises used: MeasureTheory.integral_div, ProbabilityTheory.integral_tilted_mul_eq_mgf, ProbabilityTheory.deriv_cgf, smul_eq_mul
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
e_f : ∀ (ω : Ω), rexp (t * X ω) / mgf X μ t * X ω = X ω * rexp (t * X ω) / mgf X μ t
⊢ Eq (α := ℝ) (∫ (ω : Ω), rexp (t * X ω) / mgf X μ t * X ω ∂μ) (∫ (a : Ω), X a * rexp (t * X a) / mgf X μ t ∂μ)

Tactic:
congr with ω
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
ω : Ω
⊢ rexp (t * X ω) / mgf X μ t * X ω = X ω * rexp (t * X ω) / mgf X μ t

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
⊢ AEMeasurable X μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet ht
-- Module: Mathlib.Probability.Moments.Tilted
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)
neg : ∀ (hp : ¬p = 0), MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)
⊢ MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Probability.Moments.Tilted
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)

Tactic:
simpa [hp] using hX.aestronglyMeasurable.mono_ac (tilted_absolutelyContinuous _ _)

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.tilted_absolutelyContinuous
-- Module: Mathlib.Probability.Moments.Tilted
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)

Tactic:
⟨hX.aestronglyMeasurable.mono_ac (tilted_absolutelyContinuous _ _), ?_⟩

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.MemLp, And.intro, MeasureTheory.tilted_absolutelyContinuous
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
neg : eLpNorm X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x) < ∞
⊢ MemLp X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x)

Tactic:
refine ⟨hX.aestronglyMeasurable.mono_ac (tilted_absolutelyContinuous _ _), ?_⟩
-- Module: Mathlib.Probability.Moments.Tilted
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
neg₂ : (↑p : ℝ≥0∞) ≠ ∞
⊢ eLpNorm X (↑p : ℝ≥0∞) (μ.tilted fun (x : Ω) ↦ t * X x) < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top]

Premises used: MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (↑p : ℝ≥0∞) ≠ 0

Tactic:
simp [hp]
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (↑p : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
neg : (∫⁻ (a : Ω), ENNReal.ofReal (|X a| ^ (↑p : ℝ)) ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂μ.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]

Premises used: ENNReal.coe_toReal, ENNReal.ofReal_rpow_of_nonneg, ofReal_norm, abs_nonneg, Real.norm_eq_abs, Subtype.property
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (|X a| ^ (↑p : ℝ)) ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞

Tactic:
Integrable.lintegral_lt_top ?_

Premises used: MeasureTheory.Integrable.lintegral_lt_top
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
neg : Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ (↑p : ℝ)) (μ.tilted fun (x : Ω) ↦ t * X x)
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (|X a| ^ (↑p : ℝ)) ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞

Tactic:
refine Integrable.lintegral_lt_top ?_

Premises used: MeasureTheory.Integrable.lintegral_lt_top
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
neg : Integrable (ε := ℝ) (fun (x : Ω) ↦ |X x| ^ (↑p : ℝ) * rexp (t * X x)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ (↑p : ℝ)) (μ.tilted fun (x : Ω) ↦ t * X x)

Tactic:
simp_rw [integrable_tilted_iff (interior_subset (s := integrableExpSet X μ) ht),
    smul_eq_mul, mul_comm]

Premises used: interior_subset, MeasureTheory.integrable_tilted_iff, mul_comm, smul_eq_mul
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ |X x| ^ (↑p : ℝ) * rexp (t * X x)) μ

Tactic:
integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet ht p.2

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet, Subtype.property
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ |X x| ^ (↑p : ℝ) * rexp (t * X x)) μ

Tactic:
exact integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet ht p.2

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet, Subtype.property
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
rw :
  (∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ.tilted fun (x : Ω) ↦ t * X x) 2 ∂μ.tilted fun (x : Ω) ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t
rw₁ : AEMeasurable X (μ.tilted fun (x : Ω) ↦ t * X x)
⊢ Var[X; μ.tilted fun (x : Ω) ↦ t * X x] = iteratedDeriv 2 (cgf X μ) t

Tactic:
rw [variance_eq_integral]

Premises used: ProbabilityTheory.variance_eq_integral
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X (μ.tilted fun (x : Ω) ↦ t * X x)

Tactic:
(memLp_tilted_mul ht 1).aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.memLp_tilted_mul, MeasureTheory.MemLp.aestronglyMeasurable, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X (μ.tilted fun (x : Ω) ↦ t * X x)

Tactic:
exact (memLp_tilted_mul ht 1).aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.memLp_tilted_mul, MeasureTheory.MemLp.aestronglyMeasurable, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
rw :
  Eq (α := ℝ) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 ∂μ)
    (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - deriv (cgf X μ) t) 2 * rexp (t * X a) / mgf X μ t ∂μ)
⊢ (∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ.tilted fun (x : Ω) ↦ t * X x) 2 ∂μ.tilted fun (x : Ω) ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t

Tactic:
rw [integral_tilted_mul_self ht, iteratedDeriv_two_cgf_eq_integral ht, integral_tilted_mul_eq_mgf,
    ← integral_div]

Premises used: MeasureTheory.integral_div, ProbabilityTheory.integral_tilted_mul_eq_mgf, ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral, ProbabilityTheory.integral_tilted_mul_self
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
e_f :
  ∀ (ω : Ω),
    rexp (t * X ω) / mgf X μ t * HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 =
      HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 * rexp (t * X ω) / mgf X μ t
⊢ Eq (α := ℝ) (∫ (ω : Ω), rexp (t * X ω) / mgf X μ t * HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 ∂μ)
    (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - deriv (cgf X μ) t) 2 * rexp (t * X a) / mgf X μ t ∂μ)

Tactic:
congr with ω
-- Module: Mathlib.Probability.Moments.Tilted
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
ω : Ω
⊢ rexp (t * X ω) / mgf X μ t * HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 =
    HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 * rexp (t * X ω) / mgf X μ t

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
simp_rw :
  ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 ∂μ =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖Y ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 ∂μ
⊢ eVar[X; μ] = eVar[Y; μ]

Tactic:
simp_rw [evariance, integral_congr_ae h]

Premises used: MeasureTheory.integral_congr_ae, ProbabilityTheory.evariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
h₁ :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) fun (a : Ω) ↦
    HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 ∂μ =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖Y ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
⊢ HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 = HPow.hPow (β := ℕ) ‖Y ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
h₁ :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq (α := ℝ≥0∞) ((fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) x)
                    ((fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) x))
                x}
            x}
      a
h₂ h₃ :
  ∀ (ω : Ω) (hω : X ω = Y ω),
    HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 = HPow.hPow (β := ℕ) ‖Y ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) fun (a : Ω) ↦
    HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2

Tactic:
filter_upwards [h] with ω hω using by simp [hω]