awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ
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 : ℝ)
⊢ m = ∫ (x : E), x ∂μ
have left : ∀ (g : StrongDual ℝ E), Eq (α := ℝ) ((g : (a : E) → ℝ) m : ℝ) ((g : (a : E) → ℝ) (∫ (x : E), x ∂μ) : ℝ)
Tactic: rw [SeparatingDual.eq_iff_forall_dual_eq (R := ℝ)]
-- 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 μ
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 : ℝ)
⊢ f = covarianceBilinDual μ
have right : f.toBilinForm = toBilinForm (covarianceBilinDual μ)
Tactic: rw [← toBilinForm_inj]
-- 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 μ
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 : ℝ)
⊢ f.toBilinForm = toBilinForm (covarianceBilinDual μ)
have 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 :
      ℝ)
Tactic: apply LinearMap.BilinForm.ext_of_isSymm hf.isSymm isPosSemidef_covarianceBilinDual.isSymm
-- 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
ν : 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 ν)
⊢ μ = ν
have h : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
Tactic: apply Measure.ext_of_charFunDual
-- 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
ν : 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 ν)
⊢ Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
have h : ∀ (L : StrongDual ℝ E), charFunDual μ L = charFunDual ν L
Tactic: ext L
-- 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
ν : 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
⊢ charFunDual μ L = charFunDual ν L
have 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)
Tactic: simp_rw [IsGaussian.charFunDual_eq', hm, hv]
-- 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
ν : 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)
⊢ charFunDual μ L = charFunDual ν L
have 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)
Tactic: simp_rw [IsGaussian.charFunDual_eq', hm, hv]
-- 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 : InnerProductSpace ℝ E
inst_6 : IsGaussian μ
t : E
⊢ charFun μ t =
    cexp
      ((↑⟪t, ∫ (x : E), id x ∂μ⟫ : ℂ) * I -
        (↑((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
have 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)
Tactic: rw [IsGaussian.charFun_eq, covarianceBilin_self, integral_complex_ofReal,
    integral_inner]
-- 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 : 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)
⊢ charFun μ t =
    cexp
      ((↑⟪t, ∫ (x : E), id x ∂μ⟫ : ℂ) * I -
        (↑((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
have hf : Integrable (ε := E) (fun (x : E) ↦ x) μ
Tactic: rw [IsGaussian.charFun_eq, covarianceBilin_self, integral_complex_ofReal,
    integral_inner]
-- 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 : 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) μ
⊢ charFun μ t =
    cexp
      ((↑⟪t, ∫ (x : E), id x ∂μ⟫ : ℂ) * I -
        (↑((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
have h : MemLp id 2 μ
Tactic: rw [IsGaussian.charFun_eq, covarianceBilin_self, integral_complex_ofReal,
    integral_inner]
-- 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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
⊢ 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)
have 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)
Tactic: rw [isGaussian_iff_gaussian_charFunDual]
-- 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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
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)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ
have this : ∀ (L : StrongDual ℝ E),
  charFunDual μ L =
    cexp
      ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
        (↑((((g : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2)
Tactic: have : ∀ L : StrongDual ℝ E, charFunDual μ L = exp (L m * I - g L L / 2) := by
    simp [← charFun_toDual_symm_eq_charFunDual, h, g]
-- 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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
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)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
this :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((g : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ
have hg : g.toBilinForm.IsPosSemidef
Tactic: have hg : g.toBilinForm.IsPosSemidef :=
    ⟨⟨fun x y ↦ by simpa [g] using hf.eq ..⟩, ⟨fun x ↦ by simpa [g] using hf.nonneg _⟩⟩
-- 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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
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)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
this :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((g : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
hg : g.toBilinForm.IsPosSemidef
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ
have this₁ : m = ∫ (x : E), x ∂μ ∧ g = covarianceBilinDual μ
Tactic: have := gaussian_charFunDual_congr hg this
-- 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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
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)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
this_1 :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((g : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
hg : g.toBilinForm.IsPosSemidef
this : m = ∫ (x : E), x ∂μ ∧ g = covarianceBilinDual μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ
have refine : f = covarianceBilin μ
Tactic: refine ⟨this.1, ?_⟩
-- 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 : InnerProductSpace ℝ E
inst_6 : IsFiniteMeasure μ
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)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
this_1 :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((g : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
hg : g.toBilinForm.IsPosSemidef
this : m = ∫ (x : E), x ∂μ ∧ g = covarianceBilinDual μ
⊢ f = covarianceBilin μ
have h₁ : ∀ (x x_1 : E),
  Eq (α := ℝ) ((((f : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)
Tactic: ext
-- 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 : InnerProductSpace ℝ E
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
hm : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν)
hv : Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin μ) (covarianceBilin ν)
⊢ μ = ν
have h : charFun μ = charFun ν
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 : InnerProductSpace ℝ E
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
hm : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν)
hv : Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin μ) (covarianceBilin ν)
⊢ charFun μ = charFun ν
have h : ∀ (t : E), charFun μ t = charFun ν 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 : InnerProductSpace ℝ E
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
hm : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν)
hv : Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin μ) (covarianceBilin ν)
t : E
⊢ charFun μ t = charFun ν t
have h : cexp
    ((↑⟪t, ∫ (x : E), id x ∂μ⟫ : ℂ) * I -
      (↑((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2) =
  cexp
    ((↑⟪t, ∫ (x : E), id x ∂ν⟫ : ℂ) * I -
      (↑((((covarianceBilin ν : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
Tactic: simp_rw [IsGaussian.charFun_eq', hm, hv]
-- 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 : InnerProductSpace ℝ E
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
hm : Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν)
hv : Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin μ) (covarianceBilin ν)
t : E
h :
  cexp
      ((↑⟪t, ∫ (x : E), id x ∂μ⟫ : ℂ) * I -
        (↑((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2) =
    cexp
      ((↑⟪t, ∫ (x : E), id x ∂ν⟫ : ℂ) * I -
        (↑((((covarianceBilin ν : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
⊢ charFun μ t = charFun ν t
have h₁ : cexp
    ((↑⟪t, ∫ (x : E), id x ∂ν⟫ : ℂ) * I -
      (↑((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2) =
  cexp
    ((↑⟪t, ∫ (x : E), id x ∂ν⟫ : ℂ) * I -
      (↑((((covarianceBilin ν : (a : E) → E →L[ℝ] ℝ) t : E →L[ℝ] ℝ) : (a : E) → ℝ) t) : ℂ) / 2)
Tactic: simp_rw [IsGaussian.charFun_eq', hm, hv]