awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
      ∏ i : ι,
        charFunDual (μ i)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))
refine :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
        (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i)) ν) L =
      charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
        (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i))
          (Measure.pi (α := E) μ))
        L
⊢ ν = Measure.pi (α := E) μ

Tactic:
refine (MeasurableEquiv.toLp p (Π i, E i)).map_measurableEquiv_injective
      <| Measure.ext_of_charFunDual <| funext fun L ↦ ?_

Premises used: MeasurableEquiv.toLp, funext, MeasureTheory.Measure.ext_of_charFunDual, MeasurableEquiv.map_measurableEquiv_injective
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
      ∏ i : ι,
        charFunDual (μ i)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))
L : StrongDual ℝ (WithLp p ((i : ι) → E i))
rw :
  charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L
rw₁ :
  ∏ i : ι,
      charFunDual (μ i)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
            (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
            (ContinuousLinearMap.single ℝ E i))) =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L
rw₂ rw₃ :
  Eq (α := ℂ)
    (∏ i : ι,
      charFunDual (μ i)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
            (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
            (ContinuousLinearMap.single ℝ E i))))
    (∏ i : ι,
      charFunDual (μ i)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
            (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
            (ContinuousLinearMap.single ℝ E i))))
⊢ charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i)) ν) L =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      L

Tactic:
rw [MeasurableEquiv.coe_toLp, h, charFunDual_pi']

Premises used: MeasureTheory.charFunDual_pi', MeasurableEquiv.coe_toLp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
rw :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L =
      ∏ i : ι,
        charFunDual (μ i)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))
⊢ ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
      ∏ i : ι,
        charFunDual (μ i)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L =
      ∏ i : ι,
        charFunDual (μ i)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))

Tactic:
charFunDual_pi' p

Premises used: MeasureTheory.charFunDual_pi'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L =
      ∏ i : ι,
        charFunDual (μ i)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))

Tactic:
exact charFunDual_pi' p

Premises used: MeasureTheory.charFunDual_pi'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
simp_rw :
  ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ ∗ ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)
⊢ charFunDual (μ ∗ ν) L = charFunDual μ L * charFunDual ν L

Tactic:
simp_rw [charFunDual_apply]

Premises used: MeasureTheory.charFunDual_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
rw :
  ∫ (x : E), ∫ (y : E), cexp ((↑((L : (a : E) → ℝ) (x + y)) : ℂ) * I) ∂ν ∂μ =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)
rw₁ : Integrable (ε := ℂ) (fun (v : E) ↦ cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I)) (μ ∗ ν)
⊢ ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ ∗ ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)

Tactic:
rw [integral_conv]

Premises used: MeasureTheory.integral_conv
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ ∫ (x : E), ∫ (y : E), cexp ((↑((L : (a : E) → ℝ) (x + y)) : ℂ) * I) ∂ν ∂μ =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)

Tactic:
simp [add_mul, Complex.exp_add, integral_const_mul, integral_mul_const]

Premises used: add_mul, MeasureTheory.integral_const_mul, Complex.exp_add, MeasureTheory.integral_mul_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (β := ℂ) (fun (v : E) ↦ cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I)) (μ ∗ ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ ∀ᵐ (a : E) ∂μ ∗ ν, ‖cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I)‖ ≤ Norm.norm (E := ℝ) 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ Integrable (ε := ℂ) (fun (v : E) ↦ cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I)) (μ ∗ ν)

Tactic:
exact (integrable_const (1 : ℝ)).mono (by fun_prop) (by simp)

Premises used: MeasureTheory.Integrable.mono, OfNat.ofNat, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
simp_rw :
  ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) fun (x : E) ↦
    fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (charFun μ)

Tactic:
simp_rw [funext charFun_eq_fourierIntegral']

Premises used: MeasureTheory.charFun_eq_fourierIntegral', funext
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
⊢ ContDiff ℝ (E := E) (↑(↑n : ℕ∞) : WithTop ℕ∞) (HSMul.hSMul (-(2 * Real.pi)⁻¹))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
refine :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k * norm (E := ℂ) (1 v)) μ
⊢ ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) fun (x : E) ↦
    fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)

Tactic:
refine (contDiff_fourierIntegral (L := innerSL ℝ) fun k hk ↦ ?_).comp (by fun_prop)

Premises used: Real, innerSL, VectorFourier.contDiff_fourierIntegral, ContDiff.comp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
k : ℕ
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)
simp : Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k) μ
⊢ Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k * norm (E := ℂ) (1 v)) μ

Tactic:
simp only [Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one]

Premises used: CStarRing.norm_of_mem_unitary, Pi.one_apply, OneMemClass.one_mem, mul_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
k : ℕ
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)
⊢ LE.le (α := ENNReal) (↑k : ENNReal) (↑n : ENNReal)

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
k : ℕ
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)
⊢ Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k) μ

Tactic:
refine MemLp.integrable_norm_pow' (hint.mono_exponent (by simp_all))

Premises used: MeasureTheory.MemLp.mono_exponent, MeasureTheory.MemLp.integrable_norm_pow'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
simp_rw :
  ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) fun (x : E) ↦
    fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (charFun μ)

Tactic:
simp_rw [funext charFun_eq_fourierIntegral']

Premises used: MeasureTheory.charFun_eq_fourierIntegral', funext
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
⊢ ContDiff ℝ (E := E) (↑n : WithTop ℕ∞) (HSMul.hSMul (-(2 * Real.pi)⁻¹))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
refine : ∀ (k : ℕ) (hk : (↑k : ℕ∞) ≤ n), Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k * norm (E := ℂ) (1 v)) μ
⊢ ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) fun (x : E) ↦
    fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)

Tactic:
refine (contDiff_fourierIntegral (L := innerSL ℝ) fun k hk ↦ ?_).comp (by fun_prop)

Premises used: Real, innerSL, VectorFourier.contDiff_fourierIntegral, ContDiff.comp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
k : ℕ
hk : (↑k : ℕ∞) ≤ n
simp : Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k) μ
⊢ Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k * norm (E := ℂ) (1 v)) μ

Tactic:
simp only [Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one]

Premises used: CStarRing.norm_of_mem_unitary, Pi.one_apply, OneMemClass.one_mem, mul_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
k : ℕ
hk : (↑k : ℕ∞) ≤ n
⊢ LE.le (α := ENNReal) (↑k : ENNReal) (↑k : ENNReal)

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
k : ℕ
hk : (↑k : ℕ∞) ≤ n
⊢ Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k) μ

Tactic:
refine MemLp.integrable_norm_pow' ((hint k).mono_exponent (by simp_all))

Premises used: MeasureTheory.MemLp.mono_exponent, MeasureTheory.MemLp.integrable_norm_pow'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (charFun μ)

Tactic:
contDiff_zero.1 (contDiff_charFun ?_)

Premises used: contDiff_zero, MeasureTheory.contDiff_charFun, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 μ
refine : MemLp id (↑0 : ENNReal) μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (charFun μ)

Tactic:
refine contDiff_zero.1 (contDiff_charFun ?_)

Premises used: contDiff_zero, MeasureTheory.contDiff_charFun, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 μ
⊢ AEStronglyMeasurable id μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 μ
simpa : AEStronglyMeasurable id μ
⊢ MemLp id (↑0 : ENNReal) μ

Tactic:
simpa using by fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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
⊢ Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))

Tactic:
have h : innerₗ E = (innerSL ℝ).toLinearMap₁₂ := rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 ℝ))
k : ℕ
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)
simp : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ

Tactic:
simp only [Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one]

Premises used: CStarRing.norm_of_mem_unitary, Pi.one_apply, OneMemClass.one_mem, mul_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 ℝ))
k : ℕ
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)
⊢ LE.le (α := ENNReal) (↑k : ENNReal) (↑n : ENNReal)

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 ℝ))
k : ℕ
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k) μ

Tactic:
refine MemLp.integrable_norm_pow' (hint.mono_exponent (by simp_all))

Premises used: MeasureTheory.MemLp.mono_exponent, MeasureTheory.MemLp.integrable_norm_pow'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
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 ℝ))
⊢ ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ

Tactic:
have hint' (k : ℕ) (hk : k ≤ (n : ℕ∞)) : Integrable (fun x ↦ ‖x‖ ^ k * ‖(1 : E → ℂ) x‖) μ := by
    simp only [Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one]
    refine MemLp.integrable_norm_pow' (hint.mono_exponent (by simp_all))