awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
⊢ (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) =
    (↑(Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) : (a : E) → ℝ); μ] +
          Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)) : (a : F) → ℝ); ν]) :
      ℂ)
have e_z : Var[(⇑L₁ : (a : E) → ℝ); μ] + Var[(⇑L₂ : (a : F) → ℝ); ν] =
  Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) : (a : E) → ℝ); μ] +
    Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)) : (a : F) → ℝ); ν]
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsGaussian μ
L : StrongDual ℝ E
⊢ charFunDual μ L =
    cexp
      ((↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
        (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2)
have rw : Integrable id μ
Tactic: rw [IsGaussian.charFunDual_eq, covarianceBilinDual_self_eq_variance, integral_complex_ofReal,
    L.integral_comp_id_comm']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsGaussian μ
L : StrongDual ℝ E
rw : Integrable id μ
⊢ charFunDual μ L =
    cexp
      ((↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
        (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2)
have h : MemLp id 2 μ
Tactic: rw [IsGaussian.charFunDual_eq, covarianceBilinDual_self_eq_variance, integral_complex_ofReal,
    L.integral_comp_id_comm']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
⊢ IsGaussian μ ↔
    ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
      f.toBilinForm.IsPosSemidef ∧
        ∀ (L : StrongDual ℝ E),
          charFunDual μ L =
            cexp
              ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
                (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L) :
                    ℂ) /
                  2)
have refine : (∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)) →
  ∀ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (hf : f.toBilinForm.IsPosSemidef)
    (h :
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2))
    (L : E →L[ℝ] ℝ),
    Measure.map (⇑L : (a : E) → ℝ) μ =
      gaussianReal ((L : (a : E) → ℝ) m)
        (Real.toNNReal
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L))
Tactic: refine ⟨fun h ↦ ⟨μ[id], covarianceBilinDual μ, isPosSemidef_covarianceBilinDual,
    h.charFunDual_eq'⟩,
    fun ⟨m, f, hf, h⟩ ↦ isGaussian_of_map_eq_gaussianReal fun L ↦ ⟨L m, (f L L).toNNReal, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
⊢ Measure.map (⇑L : (a : E) → ℝ) μ =
    gaussianReal ((L : (a : E) → ℝ) m)
      (Real.toNNReal
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
          L))
have h₁ : charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) =
  charFun
    (gaussianReal ((L : (a : E) → ℝ) m)
      (Real.toNNReal
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
          L)))
Tactic: apply Measure.ext_of_charFun
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) =
    charFun
      (gaussianReal ((L : (a : E) → ℝ) m)
        (Real.toNNReal
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L)))
have h₁ : ∀ (t : ℝ),
  charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) t =
    charFun
      (gaussianReal ((L : (a : E) → ℝ) m)
        (Real.toNNReal
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L)))
      t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) t =
    charFun
      (gaussianReal ((L : (a : E) → ℝ) m)
        (Real.toNNReal
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L)))
      t
have h₁ : cexp
    ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
      (↑(t *
              HMul.hMul (β := ℝ) t
                ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    L :
                  ℝ)) :
          ℂ) /
        2) =
  cexp
    ((↑t : ℂ) * (↑((L : (a : E) → ℝ) m) : ℂ) * I -
      (↑(↑(Real.toNNReal
                    ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L)) :
                ℝ) :
            ℂ) *
          HPow.hPow (β := ℕ) (↑t : ℂ) 2 /
        2)
Tactic: simp_rw [charFun_map_eq_charFunDual_smul, h, charFun_gaussianReal,
    smul_apply, map_smul, smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑(t *
                HMul.hMul (β := ℝ) t
                  ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L :
                    ℝ)) :
            ℂ) /
          2) =
    cexp
      ((↑t : ℂ) * (↑((L : (a : E) → ℝ) m) : ℂ) * I -
        (↑(↑(Real.toNNReal
                      ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L)) :
                  ℝ) :
              ℂ) *
            HPow.hPow (β := ℕ) (↑t : ℂ) 2 /
          2)
have h₁ : cexp
    ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
      (↑(t *
              HMul.hMul (β := ℝ) t
                ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    L :
                  ℝ) /
            2) :
        ℂ)) =
  cexp
    ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
      (↑((↑(Real.toNNReal
                    ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L)) :
                ℝ) *
              HPow.hPow (β := ℕ) t 2 /
            2) :
        ℂ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑(t *
                HMul.hMul (β := ℝ) t
                  ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L :
                    ℝ) /
              2) :
          ℂ)) =
    cexp
      ((↑(HMul.hMul (β := ℝ) t ((L : (a : E) → ℝ) m : ℝ)) : ℂ) * I -
        (↑((↑(Real.toNNReal
                      ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L)) :
                  ℝ) *
                HPow.hPow (β := ℕ) t 2 /
              2) :
          ℂ))
have h₁ : t *
      HMul.hMul (β := ℝ) t
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ) /
    2 =
  (↑(Real.toNNReal
            ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                (a : StrongDual ℝ E) → ℝ)
              L)) :
        ℝ) *
      HPow.hPow (β := ℕ) t 2 /
    2
Tactic: congrm exp (_ - ofReal ?_)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ t *
        HMul.hMul (β := ℝ) t
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
              L :
            ℝ) /
      2 =
    (↑(Real.toNNReal
              ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L)) :
          ℝ) *
        HPow.hPow (β := ℕ) t 2 /
      2
have h₁ : t *
      HMul.hMul (β := ℝ) t
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ) /
    2 =
  HMul.hMul (α := ℝ)
      ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ) L :
        ℝ)
      (HPow.hPow (β := ℕ) t 2) /
    2
Tactic: rw [Real.coe_toNNReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
t : ℝ
h₁ :
  t *
        HMul.hMul (β := ℝ) t
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
              L :
            ℝ) /
      2 =
    HMul.hMul (α := ℝ)
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ)
        (HPow.hPow (β := ℕ) t 2) /
      2
⊢ t *
        HMul.hMul (β := ℝ) t
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
              L :
            ℝ) /
      2 =
    (↑(Real.toNNReal
              ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L)) :
          ℝ) *
        HPow.hPow (β := ℕ) t 2 /
      2
have h₂ : LE.le (α := ℝ) (0 : ℝ)
  ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ) L : ℝ)
Tactic: rw [Real.coe_toNNReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
have h' : IsGaussian μ
Tactic: have h' := isGaussian_iff_gaussian_charFunDual.2 ⟨m, f, hf, h⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
h' : IsGaussian μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
have h₁ : ∀ (L : StrongDual ℝ E),
  ∃ (n : ℤ),
    (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
        (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2 =
      (↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2 +
        (↑n : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: simp_rw [h'.charFunDual_eq', Complex.exp_eq_exp_iff_exists_int] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.CharFun (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : SecondCountableTopology E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
h :
  ∀ (L : StrongDual ℝ E),
    ∃ (n : ℤ),
      (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
          (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2 =
        (↑((L : (a : E) → ℝ) m) : ℂ) * I -
            (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    L) :
                ℂ) /
              2 +
          (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
have choose : ∀ (n : (L : StrongDual ℝ E) → ℤ)
  (hn :
    ∀ (L : StrongDual ℝ E),
      (↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
          (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2 =
        (↑((L : (a : E) → ℝ) m) : ℂ) * I -
            (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                      (a : StrongDual ℝ E) → ℝ)
                    L) :
                ℂ) /
              2 +
          (↑(n L) : ℂ) * (2 * (↑π : ℂ) * I)),
  m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
Tactic: choose n hn using h
Cleared hypotheses: h