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 : 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 : StrongDual ℝ E
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((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) → ℝ)
        x :
      ℝ)

Tactic:
simpa using hf.nonneg _

Premises used: LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg
-- 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)
⊢ ∀ (t : E),
    charFun μ t =
      cexp
        ((↑⟪t, m⟫ : ℂ) * I -
          (↑((((f.bilinearComp (LinearIsometry.toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E))
                            (LinearIsometry.toContinuousLinearMap (InnerProductSpace.toDualMap ℝ E)) :
                          (a : E) → E →L[ℝ] ℝ)
                        t :
                      E →L[ℝ] ℝ) :
                    (a : E) → ℝ)
                  t) :
              ℂ) /
            2)

Tactic:
simp [charFun_eq_charFunDual_toDualMap, h, -InnerProductSpace.toContinuousLinearMap_toDualMap]

Premises used: InnerProductSpace.toContinuousLinearMap_toDualMap, MeasureTheory.charFun_eq_charFunDual_toDualMap
-- 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)
⊢ ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f.bilinearComp
                            (LinearIsometry.toContinuousLinearMap
                              (LinearIsometryEquiv.toLinearIsometry
                                (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))))
                            (LinearIsometry.toContinuousLinearMap
                              (LinearIsometryEquiv.toLinearIsometry
                                (LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E)))) :
                          (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
                        L :
                      StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)

Tactic:
simp [← charFun_toDual_symm_eq_charFunDual, h]

Premises used: MeasureTheory.charFun_toDual_symm_eq_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 : 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))))
⊢ ∀ (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:
simp [← charFun_toDual_symm_eq_charFunDual, h, g]

Premises used: MeasureTheory.charFun_toDual_symm_eq_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 : 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))))
⊢ ∀ (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]
-- 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 : 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)
x y : StrongDual ℝ E
⊢ Eq (α := ℝ)
    ((((g.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) x : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        y :
      ℝ)
    ((((g.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) y : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        x :
      ℝ)

Tactic:
simpa [g] 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 μ
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)
x : StrongDual ℝ E
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((g.toBilinForm : (a : StrongDual ℝ E) → StrongDual ℝ E →ₗ[ℝ] ℝ) x : StrongDual ℝ E →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        x :
      ℝ)

Tactic:
simpa [g] using hf.nonneg _

Premises used: LinearMap.BilinForm.IsNonneg.nonneg, LinearMap.BilinForm.IsPosSemidef.isNonneg
-- 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 : 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)
⊢ 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 _⟩⟩
-- 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 : 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 ∂μ ∧ g = covarianceBilinDual μ

Tactic:
have := gaussian_charFunDual_congr hg this
-- 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 : 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 μ

Tactic:
⟨this.1, ?_⟩

Premises used: And.left, And.intro
-- 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 : 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 μ
refine : f = covarianceBilin μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ

Tactic:
refine ⟨this.1, ?_⟩
-- 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 : 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 μ
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 : ℝ)
⊢ f = covarianceBilin μ

Tactic:
ext
-- 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 : 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 μ
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:
simp [covarianceBilin, ← this.2, g, ← InnerProductSpace.toDual_apply_eq_toDualMap_apply,
    -InnerProductSpace.toContinuousLinearMap_toDualMap]

Premises used: ProbabilityTheory.covarianceBilin, And.right, InnerProductSpace.toContinuousLinearMap_toDualMap, InnerProductSpace.toDual_apply_eq_toDualMap_apply
-- 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
ν : 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 ν)
h : charFun μ = charFun ν
⊢ μ = ν

Tactic:
apply Measure.ext_of_charFun

Premises used: MeasureTheory.Measure.ext_of_charFun
-- 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
ν : 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 ν)
h : ∀ (t : E), charFun μ t = charFun ν t
⊢ charFun μ = charFun ν

Tactic:
ext t
-- 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
ν : 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)
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

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

Premises used: 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
ν : Measure E
inst_6 : IsGaussian μ
inst_7 : IsGaussian ν
h : μ = ν
⊢ Eq (α := E) (∫ (x : E), id x ∂μ) (∫ (x : E), id x ∂ν) ∧
    Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin μ) (covarianceBilin ν)

Tactic:
simp [h]
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp (-(↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)

Tactic:
simp [charFunDual_eq L, integral_complex_ofReal, hμ L, neg_div]

Premises used: neg_div, ProbabilityTheory.IsGaussian.charFunDual_eq, integral_complex_ofReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
⊢ Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ

Tactic:
Measure.ext_of_charFunDual ?_

Premises used: MeasureTheory.Measure.ext_of_charFunDual
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
refine :
  Eq (α := (L : StrongDual ℝ (E × E)) → ℂ)
    (charFunDual (mE := Prod.instMeasurableSpace)
      (Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ)))
    (charFunDual (μ.prod μ))
⊢ Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ

Tactic:
refine Measure.ext_of_charFunDual ?_

Premises used: MeasureTheory.Measure.ext_of_charFunDual