awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 =
    ∑ k ∈ Finset.range (2 + 1),
      (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k *
        (↑(@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (x : ℝ) ↦ x ^ k) : ℂ)

Tactic:
taylorWithinEval_charFun_zero hint t

Premises used: MeasureTheory.taylorWithinEval_charFun_zero
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 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) : ℂ)
⊢ 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

Tactic:
convert! taylorWithinEval_charFun_zero hint t with x

Premises used: MeasureTheory.taylorWithinEval_charFun_zero
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 * (↑(@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) : ℂ)
⊢ 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:
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]

Premises used: Nat.cast_ofNat, inv_one, Nat.reduceAdd, Complex.ofReal_one, pow_zero, Finset.sum_singleton, Nat.factorial_two, Pi.pow_apply, pow_one, MeasureTheory.integral_const, MeasureTheory.probReal_univ, Finset.range_one, Nat.factorial_zero, smul_eq_mul, mul_one, Nat.cast_one, Finset.sum_range_succ, one_mul, Nat.factorial_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
h₄ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ x) (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) : ℂ)

Tactic:
rw [integral_map, integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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)
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ x) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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) * 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) : ℂ))
⊢ 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:
simp [field]
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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) * 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:
ring
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
⊢ taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 t =
    1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2

Tactic:
rw [taylorWithinEval_charFun_two_zero hX, h0, h1]

Premises used: MeasureTheory.taylorWithinEval_charFun_two_zero
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℝ
⊢ 1 + (↑0 : ℂ) * (↑t : ℂ) * I - (↑1 : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 = 1 - HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℝ
⊢ AEStronglyMeasurable (m₀ := Real.measurableSpace) id (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0
⊢ MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)

Tactic:
refine (memLp_two_iff_integrable_sq (by fun_prop)).2 (.of_integral_ne_zero ?_)

Premises used: Iff.mpr, MeasureTheory.Integrable.of_integral_ne_zero, MeasureTheory.memLp_two_iff_integrable_sq
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
hint₂ :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2)
    (Measure.map X P)
⊢ Ne (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0

Tactic:
rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℝ
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2)
    (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (id (X x)) 2 ∂P) 0

Tactic:
simp [← Pi.pow_apply, h1]

Premises used: Pi.pow_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
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
⊢ 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

Tactic:
simp_rw [← taylorWithinEval_charFun_two_zero' (by fun_prop) h0 h1]

Premises used: MeasureTheory.taylorWithinEval_charFun_two_zero'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 (x : ℝ) ↦
      charFun (mE := Real.measurableSpace) (Measure.map X P) x -
        taylorWithinEval (charFun (mE := Real.measurableSpace) (Measure.map X P)) 2 univ 0 x)
    fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (x - 0) 2

Tactic:
taylor_isLittleO_univ ?_

Premises used: taylor_isLittleO_univ
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
convert_7 : ContDiff ℝ (↑2 : WithTop ℕ∞) (charFun (mE := Real.measurableSpace) (Measure.map X P))
⊢ 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:
convert! taylor_isLittleO_univ ?_

Premises used: taylor_isLittleO_univ
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
x : ℝ
⊢ x = x - 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
⊢ AEStronglyMeasurable (m₀ := Real.measurableSpace) id (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0
⊢ ContDiff ℝ (↑2 : WithTop ℕ∞) (charFun (mE := Real.measurableSpace) (Measure.map X P))

Tactic:
refine contDiff_charFun <|
    (memLp_two_iff_integrable_sq (by fun_prop)).2 (.of_integral_ne_zero ?_)

Premises used: Iff.mpr, MeasureTheory.Integrable.of_integral_ne_zero, MeasureTheory.memLp_two_iff_integrable_sq, MeasureTheory.contDiff_charFun
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
convert_7₂ :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2)
    (Measure.map X P)
⊢ Ne (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X P) fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2) 0

Tactic:
rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (a : ℝ) ↦ HPow.hPow (β := ℕ) (id a) 2)
    (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) (id (X x)) 2 ∂P) 0

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.Comap
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 α
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∞)
⊢ (((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∞)

Tactic:
simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1]

Premises used: MeasureTheory.OuterMeasure.comap_apply, Set.image_diff, Set.image_inter, And.left
-- Module: Mathlib.MeasureTheory.Measure.Comap
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 α
a : MeasurableSet (f '' s)
⊢ (μ.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:
apply le_toOuterMeasure_caratheodory

Premises used: MeasureTheory.le_toOuterMeasure_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.Comap
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 α
⊢ MeasurableSet (f '' s)

Tactic:
hf.2 s hs

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Comap
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 α
⊢ MeasurableSet (f '' s)

Tactic:
exact hf.2 s hs

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
x : MeasurableSpace α
x_1 : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
⟨hfi, hf⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
s : Set α
x : MeasurableSpace α
x_1 : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
exact ⟨hfi, hf⟩
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
t : Set α
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∞)
⊢ (((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∞)

Tactic:
simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1]

Premises used: MeasureTheory.OuterMeasure.comap_apply, Set.image_diff, Set.image_inter, And.left
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
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∞)

Tactic:
(measure_inter_add_diff₀ _ (hf.2 s hs)).symm

Premises used: MeasureTheory.measure_inter_add_diff₀, And.right, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Comap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
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∞)

Tactic:
exact (measure_inter_add_diff₀ _ (hf.2 s hs)).symm

Premises used: MeasureTheory.measure_inter_add_diff₀, And.right, Eq.symm