awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 μ
n : (L : StrongDual ℝ E) → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    (↑(n L) : ℂ) =
      ((↑((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) /
        (2 * (↑π : ℂ) * I)
this_1 : Continuous n
this_2 : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn :
  ∀ (L : StrongDual ℝ E),
    Eq (α := ℝ)
        ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ)
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ) ∧
      Eq (α := ℝ) ((L : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ) ((L : (a : E) → ℝ) m : ℝ)
⊢ ∀ (g : StrongDual ℝ E), Eq (α := ℝ) ((g : (a : E) → ℝ) m : ℝ) ((g : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ)

Tactic:
simp [hn]
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 μ
n : (L : StrongDual ℝ E) → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    (↑(n L) : ℂ) =
      ((↑((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) /
        (2 * (↑π : ℂ) * I)
this_1 : Continuous n
this_2 : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn :
  ∀ (L : StrongDual ℝ E),
    Eq (α := ℝ)
        ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ)
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ) ∧
      Eq (α := ℝ) ((L : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ) ((L : (a : E) → ℝ) m : ℝ)
right : f.toBilinForm = toBilinForm (covarianceBilinDual μ)
⊢ f = covarianceBilinDual μ

Tactic:
rw [← toBilinForm_inj]

Premises used: ContinuousLinearMap.toBilinForm_inj
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 μ
n : (L : StrongDual ℝ E) → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    (↑(n L) : ℂ) =
      ((↑((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) /
        (2 * (↑π : ℂ) * I)
this_1 : Continuous n
this_2 : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn :
  ∀ (L : StrongDual ℝ E),
    Eq (α := ℝ)
        ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ)
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ) ∧
      Eq (α := ℝ) ((L : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ) ((L : (a : E) → ℝ) m : ℝ)
right :
  ∀ (x : StrongDual ℝ E),
    Eq (α := ℝ)
      ((((f.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) x : StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          x :
        ℝ)
      ((((toBilinForm (covarianceBilinDual μ) : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) x :
              StrongDual ℝ E →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          x :
        ℝ)
⊢ f.toBilinForm = toBilinForm (covarianceBilinDual μ)

Tactic:
apply LinearMap.BilinForm.ext_of_isSymm hf.isSymm isPosSemidef_covarianceBilinDual.isSymm

Premises used: LinearMap.BilinForm.IsPosSemidef.isSymm, ProbabilityTheory.isPosSemidef_covarianceBilinDual, LinearMap.BilinForm.ext_of_isSymm
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 μ
n : (L : StrongDual ℝ E) → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    (↑(n L) : ℂ) =
      ((↑((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) /
        (2 * (↑π : ℂ) * I)
this_1 : Continuous n
this_2 : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn :
  ∀ (L : StrongDual ℝ E),
    Eq (α := ℝ)
        ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ)
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L :
          ℝ) ∧
      Eq (α := ℝ) ((L : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ) ((L : (a : E) → ℝ) m : ℝ)
x : StrongDual ℝ E
⊢ Eq (α := ℝ)
    ((((f.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) x : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        x :
      ℝ)
    ((((toBilinForm (covarianceBilinDual μ) : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) x :
            StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        x :
      ℝ)

Tactic:
simp [covarianceBilinDual_self_eq_variance IsGaussian.memLp_two_id, (hn x).1.symm]

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id, ProbabilityTheory.covarianceBilinDual_self_eq_variance, And.left, Eq.symm
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
hm : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν)
hv : Eq (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (covarianceBilinDual μ) (covarianceBilinDual ν)
h : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
⊢ μ = ν

Tactic:
apply Measure.ext_of_charFunDual

Premises used: MeasureTheory.Measure.ext_of_charFunDual
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
hm : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν)
hv : Eq (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (covarianceBilinDual μ) (covarianceBilinDual ν)
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = charFunDual ν L
⊢ Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)

Tactic:
ext L
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
hm : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν)
hv : Eq (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (covarianceBilinDual μ) (covarianceBilinDual ν)
L : StrongDual ℝ E
h :
  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) =
    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)
h₁ :
  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) =
    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)
⊢ charFunDual μ L = charFunDual ν L

Tactic:
simp_rw [IsGaussian.charFunDual_eq', hm, hv]

Premises used: ProbabilityTheory.IsGaussian.charFunDual_eq'
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
h : μ = ν
⊢ Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν) ∧
    Eq (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (covarianceBilinDual μ) (covarianceBilinDual ν)

Tactic:
simp [h]
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsGaussian μ
t : E
rw :
  cexp ((↑⟪t, ∫ (x : E), x ∂μ⟫ : ℂ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2) =
    cexp ((↑⟪t, ∫ (x : E), id x ∂μ⟫ : ℂ) * I - (↑Var[fun (u : E) ↦ ⟪t, u⟫; μ] : ℂ) / 2)
hf : Integrable (ε := E) (fun (x : E) ↦ x) μ
h : MemLp id 2 μ
⊢ charFun μ t =
    cexp
      ((↑⟪t, ∫ (x : E), id x ∂μ⟫ : ℂ) * I -
        (↑((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)

Tactic:
rw [IsGaussian.charFun_eq, covarianceBilin_self, integral_complex_ofReal,
    integral_inner]

Premises used: ProbabilityTheory.covarianceBilin_self, integral_inner, integral_complex_ofReal, ProbabilityTheory.IsGaussian.charFun_eq
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsGaussian μ
t : E
⊢ cexp ((↑⟪t, ∫ (x : E), x ∂μ⟫ : ℂ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2) =
    cexp ((↑⟪t, ∫ (x : E), id x ∂μ⟫ : ℂ) * I - (↑Var[fun (u : E) ↦ ⟪t, u⟫; μ] : ℂ) / 2)

Tactic:
rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsGaussian μ
t : E
⊢ Integrable (ε := E) (fun (x : E) ↦ x) μ

Tactic:
IsGaussian.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsGaussian μ
t : E
⊢ Integrable (ε := E) (fun (x : E) ↦ x) μ

Tactic:
exact IsGaussian.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsGaussian μ
t : E
⊢ MemLp id 2 μ

Tactic:
IsGaussian.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsGaussian μ
t : E
⊢ MemLp id 2 μ

Tactic:
exact IsGaussian.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
rw :
  (∃ (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 : E →L[ℝ] E →L[ℝ] ℝ),
      f.toBilinForm.IsPosSemidef ∧
        ∀ (t : E),
          charFun μ t =
            cexp ((↑⟪t, m⟫ : ℂ) * I - (↑((((f : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
⊢ IsGaussian μ ↔
    ∃ (m : E) (f : E →L[ℝ] E →L[ℝ] ℝ),
      f.toBilinForm.IsPosSemidef ∧
        ∀ (t : E),
          charFun μ t =
            cexp ((↑⟪t, m⟫ : ℂ) * I - (↑((((f : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)

Tactic:
rw [isGaussian_iff_gaussian_charFunDual]

Premises used: ProbabilityTheory.isGaussian_iff_gaussian_charFunDual
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
⊢ (∃ (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 : E →L[ℝ] E →L[ℝ] ℝ),
      f.toBilinForm.IsPosSemidef ∧
        ∀ (t : E),
          charFun μ t =
            cexp ((↑⟪t, m⟫ : ℂ) * I - (↑((((f : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)

Tactic:
⟨fun ⟨m, f, hf, h⟩ ↦ ⟨m,
    f.bilinearComp (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap
      (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap,
    ⟨⟨fun x y ↦ ?_⟩, ⟨fun x ↦ ?_⟩⟩, ?_⟩,
    fun ⟨m, f, hf, h⟩ ↦ ⟨m,
      f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
        (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap,
    ⟨⟨fun x y ↦ ?_⟩, ⟨fun x ↦ ?_⟩⟩, ?_⟩⟩

Premises used: ContinuousLinearMap.toBilinForm, InnerProductSpace.toDual, LinearIsometryEquiv.toLinearIsometry, Real, LinearIsometryEquiv.symm, _private.0.ProbabilityTheory.isGaussian_iff_gaussian_charFun.match_2, Exists, LinearMap.BilinForm.IsPosSemidef, LinearMap.BilinForm.IsSymm.mk, _private.0.ProbabilityTheory.isGaussian_iff_gaussian_charFun.match_1, LinearMap.BilinForm.IsPosSemidef.mk, InnerProductSpace.toDualMap, And, And.intro, Iff.intro, Exists.intro, LinearMap.BilinForm.IsNonneg.mk, ContinuousLinearMap.bilinearComp, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ 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)
x y : E
⊢ Eq (α := ℝ)
    (((((f.bilinearComp (LinearIsometry.toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E))
                    (LinearIsometry.toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E))).toBilinForm :
                (a : E) → E →ₗ[ℝ] ℝ)
              x :
            E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        y :
      ℝ)
    (((((f.bilinearComp (LinearIsometry.toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E))
                    (LinearIsometry.toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E))).toBilinForm :
                (a : E) → E →ₗ[ℝ] ℝ)
              y :
            E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        x :
      ℝ)

Tactic:
simpa using hf.eq ..

Premises used: LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsPosSemidef.isSymm
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : E →L[ℝ] E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (t : E),
        charFun μ t =
          cexp ((↑⟪t, m⟫ : ℂ) * I - (↑((((f : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (t : E),
    charFun μ t = cexp ((↑⟪t, m⟫ : ℂ) * I - (↑((((f : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
x y : StrongDual ℝ E
⊢ Eq (α := ℝ)
    (((((f.bilinearComp
                    (LinearIsometry.toContinuousLinearMap
                      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
                    (LinearIsometry.toContinuousLinearMap
                      (LinearIsometryEquiv.toLinearIsometry
                        (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))).toBilinForm :
                (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
              x :
            StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        y :
      ℝ)
    (((((f.bilinearComp
                    (LinearIsometry.toContinuousLinearMap
                      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
                    (LinearIsometry.toContinuousLinearMap
                      (LinearIsometryEquiv.toLinearIsometry
                        (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))).toBilinForm :
                (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
              y :
            StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        x :
      ℝ)

Tactic:
simpa using hf.eq ..

Premises used: LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsPosSemidef.isSymm
-- Module: Mathlib.Probability.Distributions.Gaussian.CharFun
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 : InnerProductSpace ℝ 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)
x : E
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((f.bilinearComp (LinearIsometry.toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E))
                    (LinearIsometry.toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E))).toBilinForm :
                (a : E) → E →ₗ[ℝ] ℝ)
              x :
            E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        x :
      ℝ)

Tactic:
simpa using hf.nonneg _

Premises used: LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg