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) → ℤ
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)
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)
have rw : (↑(n L) : ℂ) =
  ((↑((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) -
        (↑((L : (a : E) → ℝ) m) : ℂ) * I +
      (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
              L) :
          ℂ) /
        2) /
    (2 * (↑π : ℂ) * I)
Tactic: rw [hn 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
inst_6 : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
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)
L : StrongDual ℝ E
⊢ (↑(n L) : ℂ) =
    ((↑((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) -
          (↑((L : (a : E) → ℝ) m) : ℂ) * I +
        (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2) /
      (2 * (↑π : ℂ) * I)
have field_simp : (↑(n L) : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) =
  (↑((L : (a : E) → ℝ) m) : ℂ) * I * 2 -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) +
        (↑(n L) : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 2 2 * (↑π : ℂ) -
      (↑((L : (a : E) → ℝ) m) : ℂ) * I * 2 +
    (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
          L) :
      ℂ)
Tactic: field_simp
-- 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' : IsGaussian μ
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 μ
have 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)
Tactic: have h L : (n L : ℂ) = (L (∫ x, id x ∂μ) * I - covarianceBilinDual μ L L / 2 -
      L m * I + f L L / 2) / (2 * π * I) := by
    rw [hn L]
    field_simp
    ring
-- 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) → ℤ
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)
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)
⊢ Continuous n
have rw : Continuous (Y := ℂ) (Int.cast ∘ n)
Tactic: rw [← Complex.isometry_intCast.comp_continuous_iff]
-- 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) → ℤ
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)
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)
⊢ Continuous (Y := ℂ) fun (L : StrongDual ℝ E) ↦ (↑(n L) : ℂ)
have simp_rw : Continuous (Y := ℂ) fun (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) /
    (2 * (↑π : ℂ) * I)
Tactic: simp_rw [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' : IsGaussian μ
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)
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)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
have this : Continuous n
Tactic: have : Continuous n := by
    rw [← Complex.isometry_intCast.comp_continuous_iff]
    change Continuous (fun L ↦ (n L : ℂ))
    simp_rw [h]
    fun_prop
-- 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' : IsGaussian μ
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)
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 : Continuous n
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
have this₁ : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
Tactic: have := (IsLocallyConstant.iff_continuous n).2 this |>.eq_const
-- 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) → ℤ
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)
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 : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
L : StrongDual ℝ E
⊢ n L = 0
have rw : Eq (α := ℂ) (↑(Function.const (StrongDual ℝ E) (n 0) L) : ℂ) (↑0 : ℂ)
Tactic: rw [this 0, ← Int.cast_inj (α := ℂ)]
-- 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' : IsGaussian μ
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)
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 : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
have this₁ : ∀ (L : StrongDual ℝ E), n L = 0
Tactic: have this L : n L = 0 := by
    rw [this 0, ← Int.cast_inj (α := ℂ)]
    simp [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' : IsGaussian μ
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)
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
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
have 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 : ℝ)
Tactic: simp only [id_eq, this, Int.cast_zero, zero_mul, add_zero, Complex.ext_iff, sub_re, mul_re,
    ofReal_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self, div_ofNat_re, zero_sub, neg_inj,
    ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_left_inj', sub_im, mul_im, div_ofNat_im,
    zero_div, sub_zero] at hn
Cleared hypotheses: hn
-- 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 ∂μ ∧ f = covarianceBilinDual μ
have left : m = ∫ (x : E), x ∂μ
Tactic: constructor
-- 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 : ℝ)
left : m = ∫ (x : E), x ∂μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
have right : f = covarianceBilinDual μ
Tactic: constructor