awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
⊢ (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹)) ^ n *
      ∫ (v : E),
        cexp (2 * (↑Real.pi : ℂ) * ((↑Real.pi : ℂ)⁻¹ * 2⁻¹ * (↑⟪v, t⟫ : ℂ)) * I) *
          ((-(2 * (↑Real.pi : ℂ) * I)) ^ n * ∏ i : Fin n, (↑⟪v, x i⟫ : ℂ)) ∂μ =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
have simp_rw : (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹) * -(2 * (↑Real.pi : ℂ) * I)) ^ n *
    ∫ (a : E),
      cexp (2 * (↑Real.pi : ℂ) * (↑Real.pi : ℂ)⁻¹ * 2⁻¹ * (↑⟪a, t⟫ : ℂ) * I) * ∏ i : Fin n, (↑⟪a, x i⟫ : ℂ) ∂μ =
  I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
Tactic: simp_rw [mul_left_comm (exp _), integral_const_mul, ← mul_assoc, ← mul_pow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
⊢ (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹) * -(2 * (↑Real.pi : ℂ) * I)) ^ n *
      ∫ (a : E),
        cexp (2 * (↑Real.pi : ℂ) * (↑Real.pi : ℂ)⁻¹ * 2⁻¹ * (↑⟪a, t⟫ : ℂ) * I) * ∏ i : Fin n, (↑⟪a, x i⟫ : ℂ) ∂μ =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
have field_simp : Eq (α := ℂ) (∫ (a : E), cexp (I * (↑⟪a, t⟫ : ℂ)) * ∏ i : Fin n, (↑⟪a, x i⟫ : ℂ) ∂μ)
  (∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp (I * (↑⟪y, t⟫ : ℂ)) ∂μ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
⊢ Eq (α := ℂ) (∫ (a : E), cexp (I * (↑⟪a, t⟫ : ℂ)) * ∏ i : Fin n, (↑⟪a, x i⟫ : ℂ) ∂μ)
    (∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp (I * (↑⟪y, t⟫ : ℂ)) ∂μ)
have e_f : ∀ (x_1 : E),
  cexp (I * (↑⟪x_1, t⟫ : ℂ)) * ∏ i : Fin n, (↑⟪x_1, x i⟫ : ℂ) =
    (∏ i : Fin n, (↑⟪x_1, x i⟫ : ℂ)) * cexp (I * (↑⟪x_1, t⟫ : ℂ))
Tactic: congr with
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
t : ℝ
hint : MemLp id (↑n : ENNReal) μ
⊢ iteratedDeriv n (charFun μ) t = I ^ n * ∫ (x : ℝ), (↑x : ℂ) ^ n * cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ
have rw : I ^ n * ∫ (y : ℝ), (↑(∏ i : Fin n, ⟪y, 1⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ =
  I ^ n * ∫ (x : ℝ), (↑x : ℂ) ^ n * cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ
Tactic: rw [iteratedDeriv, iteratedFDeriv_charFun hint]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
⊢ iteratedDeriv n (charFun μ) 0 = I ^ n * (↑(∫ (x : ℝ), x ^ n ∂μ) : ℂ)
have simp : ∫ (x : ℝ), (↑x : ℂ) ^ n ∂μ = (↑(∫ (x : ℝ), x ^ n ∂μ) : ℂ)
Tactic: simp [iteratedDeriv_charFun hint]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
⊢ ∫ (x : ℝ), (↑x : ℂ) ^ n ∂μ = (↑(∫ (x : ℝ), x ^ n ∂μ) : ℂ)
have norm_cast : Eq (α := ℝ) (∫ (x : ℝ), x ^ n ∂μ) (∫ (x : ℝ), x ^ n ∂μ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
⊢ taylorWithinEval (charFun μ) n univ 0 t =
    ∑ k ∈ Finset.range (n + 1), (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)
have simp_rw : Eq (α := ℂ) (∑ x ∈ Finset.range (n + 1), (↑((↑x ! : ℝ)⁻¹ * t ^ x) : ℂ) * iteratedDerivWithin x (charFun μ) univ 0)
  (∑ k ∈ Finset.range (n + 1), (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ))
Tactic: simp_rw [taylor_within_apply, sub_zero, RCLike.real_smul_eq_coe_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
⊢ Eq (α := ℂ) (∑ x ∈ Finset.range (n + 1), (↑((↑x ! : ℝ)⁻¹ * t ^ x) : ℂ) * iteratedDerivWithin x (charFun μ) univ 0)
    (∑ k ∈ Finset.range (n + 1), (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ))
have refine : ∀ (k : ℕ) (hkn : k ∈ Finset.range (n + 1)),
  (↑((↑k ! : ℝ)⁻¹ * t ^ k) : ℂ) * iteratedDerivWithin k (charFun μ) univ 0 =
    (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)
Tactic: refine Finset.sum_congr rfl fun k hkn ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
k : ℕ
hkn : k ∈ Finset.range (n + 1)
⊢ (↑((↑k ! : ℝ)⁻¹ * t ^ k) : ℂ) * iteratedDerivWithin k (charFun μ) univ 0 =
    (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)
have push_cast : (↑k ! : ℂ)⁻¹ * HPow.hPow (α := ℂ) (↑t : ℂ) k * iteratedDerivWithin k (charFun μ) univ 0 =
  (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (hypothesis)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
k : ℕ
hkn : k ∈ Finset.range (n + 1)
⊢ (↑k ! : ℂ)⁻¹ * HPow.hPow (α := ℂ) (↑t : ℂ) k * iteratedDerivWithin k (charFun μ) univ 0 =
    (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)
have hint' : MemLp id (↑k : ENNReal) μ
Tactic: have hint' : MemLp id k μ := hint.mono_exponent (by simp_all)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
t : ℝ
⊢ taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 t =
    1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
have this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map X P)
Tactic: have : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map hX
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map X P)
⊢ taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 t =
    1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
have h : 1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
    (↑(∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
  ∑ k ∈ Finset.range (2 + 1),
    (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k *
      (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ x ^ k) : ℂ)
Tactic: convert! taylorWithinEval_charFun_zero hint t with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map X P)
⊢ 1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
    ∑ k ∈ Finset.range (2 + 1),
      (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k *
        (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ x ^ k) : ℂ)
have h : 1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
    (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
  1 + (↑t : ℂ) * I * (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ x) : ℂ) +
    2⁻¹ * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 *
      (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) : ℂ)
Tactic: simp only [Pi.pow_apply, Nat.reduceAdd, Finset.sum_range_succ, Finset.range_one,
    Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, mul_one,
    integral_const, probReal_univ, smul_eq_mul, ofReal_one, Nat.factorial_one, pow_one, one_mul,
    Nat.factorial_two, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map X P)
⊢ 1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
    1 + (↑t : ℂ) * I * (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ x) : ℂ) +
      2⁻¹ * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 *
        (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) : ℂ)
have h : 1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
    (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
  1 + (↑t : ℂ) * I * (↑(∫ (x : Ω), X x ∂P) : ℂ) +
    2⁻¹ * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 * (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ)
Tactic: rw [integral_map, integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map X P)
h :
  1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
    1 + (↑t : ℂ) * I * (↑(∫ (x : Ω), X x ∂P) : ℂ) +
      2⁻¹ * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 * (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ)
h₁ : AEMeasurable X P
⊢ 1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
    1 + (↑t : ℂ) * I * (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ x) : ℂ) +
      2⁻¹ * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 *
        (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) : ℂ)
have h₂ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (Measure.map X P)
Tactic: rw [integral_map, integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map X P)
h :
  1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
    1 + (↑t : ℂ) * I * (↑(∫ (x : Ω), X x ∂P) : ℂ) +
      2⁻¹ * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 * (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ)
h₁ : AEMeasurable X P
h₂ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (Measure.map X P)
h₃ : AEMeasurable X P
⊢ 1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
    1 + (↑t : ℂ) * I * (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ x) : ℂ) +
      2⁻¹ * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 *
        (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) : ℂ)
have h₄ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ x) (Measure.map X P)
Tactic: rw [integral_map, integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map X P)
⊢ 1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I -
      (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 =
    1 + (↑t : ℂ) * I * (↑(∫ (x : Ω), X x ∂P) : ℂ) +
      2⁻¹ * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 * (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ)
have h : (1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I) * 2 -
    HPow.hPow (β := ℕ) (↑t : ℂ) 2 * (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ) =
  (1 + (↑(∫ (x : Ω), X x ∂P) : ℂ) * (↑t : ℂ) * I) * 2 +
    -(HPow.hPow (β := ℕ) (↑t : ℂ) 2 * (↑(∫ (x : Ω), HPow.hPow (β := ℕ) (X x) 2 ∂P) : ℂ))
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
⊢ taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 t =
    1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
have rw : 1 + (↑0 : ℂ) * (↑t : ℂ) * I - (↑1 : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 = 1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
Tactic: rw [taylorWithinEval_charFun_two_zero hX, h0, h1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
rw : 1 + (↑0 : ℂ) * (↑t : ℂ) * I - (↑1 : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 = 1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
⊢ taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 t =
    1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
have hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
Tactic: rw [taylorWithinEval_charFun_two_zero hX, h0, h1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
⊢ MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
have hint : Ne (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0
Tactic: refine (memLp_two_iff_integrable_sq (by fun_prop)).2 (.of_integral_ne_zero ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
⊢ Ne (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0
have hint : Ne (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (id (X x)) 2 ∂P) 0
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
t : ℝ
hint : Ne (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (id (X x)) 2 ∂P) 0
hint₁ : AEMeasurable X P
⊢ Ne (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0
have hint₂ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) (Measure.map X P)
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℝ) (𝓝 0)
    (fun (t : ℝ) ↦ charFun (mE := Real.measurableSpace) (Measure.map X P) t - (1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2))
    fun (t : ℝ) ↦ HPow.hPow (β := ℕ) t 2
have simp_rw : Asymptotics.IsLittleO (E := ℂ) (F := ℝ) (𝓝 0)
  (fun (t : ℝ) ↦
    charFun (mE := Real.measurableSpace) (Measure.map X P) t -
      taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 t)
  fun (t : ℝ) ↦ HPow.hPow (β := ℕ) t 2
Tactic: simp_rw [← taylorWithinEval_charFun_two_zero' (by fun_prop) h0 h1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℝ) (𝓝 0)
    (fun (t : ℝ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) t -
        taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 t)
    fun (t : ℝ) ↦ HPow.hPow (β := ℕ) t 2
have h : ∀ (x : ℝ), x = x - 0
Tactic: convert! taylor_isLittleO_univ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
h : ∀ (x : ℝ), x = x - 0
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℝ) (𝓝 0)
    (fun (t : ℝ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) t -
        taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 t)
    fun (t : ℝ) ↦ HPow.hPow (β := ℕ) t 2
have convert_7 : ContDiff ℝ (↑2 : WithTop ℕ∞) (charFun (mE := Real.measurableSpace) (Measure.map X P))
Tactic: convert! taylor_isLittleO_univ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
⊢ ContDiff ℝ (↑2 : WithTop ℕ∞) (charFun (mE := Real.measurableSpace) (Measure.map X P))
have convert_7 : Ne (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0
Tactic: refine contDiff_charFun <|
    (memLp_two_iff_integrable_sq (by fun_prop)).2 (.of_integral_ne_zero ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
⊢ Ne (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0
have convert_7 : Ne (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (id (X x)) 2 ∂P) 0
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : Eq (α := ℝ) (∫ (x : Ω), X x ∂P) 0
h1 : Eq (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂P) 1
convert_7 : Ne (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (id (X x)) 2 ∂P) 0
convert_7₁ : AEMeasurable X P
⊢ Ne (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0
have convert_7₂ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) (Measure.map X P)
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
s : Set α
hs : MeasurableSet s
t : Set α
⊢ (((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t ∩ s) :
        ℝ≥0∞)
      ((((OuterMeasure.comap f : (a : OuterMeasure β) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t \ s) :
        ℝ≥0∞)
have simp : (μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t ∩ f '' s) : ℝ≥0∞)
    ((μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t \ f '' s) : ℝ≥0∞)
Tactic: simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
s : Set α
hs : MeasurableSet s
t : Set α
⊢ (μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t ∩ f '' s) : ℝ≥0∞)
      ((μ.toOuterMeasure : (a : Set β) → ℝ≥0∞) (f '' t \ f '' s) : ℝ≥0∞)
have a : MeasurableSet (f '' s)
Tactic: apply le_toOuterMeasure_caratheodory