awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
e_z :
  HAdd.hAdd (α := ℂ) (∫ (x : E), (↑((L₁ : (a : E) → ℝ) x) : ℂ) ∂μ) (∫ (x : F), (↑((L₂ : (a : F) → ℝ) x) : ℂ) ∂ν) * I -
      ((↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) / 2 + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) / 2) =
    (∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν) * I - (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2
⊢ (∫ (x : E),
            (↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) x) :
              ℂ) ∂μ) *
          I -
        (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) : (a : E) → ℝ); μ] :
            ℂ) /
          2 +
      ((∫ (x : F),
            (↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) x) :
              ℂ) ∂ν) *
          I -
        (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)) : (a : F) → ℝ); ν] :
            ℂ) /
          2) =
    (∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν) * I - (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2

Tactic:
rw [← hL₁, ← hL₂, sub_add_sub_comm, ← add_mul]

Premises used: add_mul, sub_add_sub_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
e_z :
  HAdd.hAdd (α := ℂ) (∫ (x : E), (↑((L₁ : (a : E) → ℝ) x) : ℂ) ∂μ) (∫ (x : F), (↑((L₂ : (a : F) → ℝ) x) : ℂ) ∂ν) =
    ∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν
e_z₁ :
  (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) / 2 + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) / 2 =
    (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2
⊢ HAdd.hAdd (α := ℂ) (∫ (x : E), (↑((L₁ : (a : E) → ℝ) x) : ℂ) ∂μ) (∫ (x : F), (↑((L₂ : (a : F) → ℝ) x) : ℂ) ∂ν) * I -
      ((↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) / 2 + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) / 2) =
    (∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν) * I - (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
e_z :
  (↑(∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ) : ℂ) + (↑(∫ (x : F), (L₂ : (a : F) → ℝ) x ∂ν) : ℂ) =
    (↑(∫ (x : E × F), (L : (a : E × F) → ℝ) x ∂μ.prod ν) : ℂ)
⊢ HAdd.hAdd (α := ℂ) (∫ (x : E), (↑((L₁ : (a : E) → ℝ) x) : ℂ) ∂μ) (∫ (x : F), (↑((L₂ : (a : F) → ℝ) x) : ℂ) ∂ν) =
    ∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν

Tactic:
simp_rw [integral_complex_ofReal]

Premises used: integral_complex_ofReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
e_z :
  (↑(∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ) : ℂ) + (↑(∫ (x : F), (L₂ : (a : F) → ℝ) x ∂ν) : ℂ) =
    (↑(HAdd.hAdd (α := ℝ)
          (∫ (x : E),
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) x ∂μ)
          (∫ (y : F),
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) y ∂ν)) :
      ℂ)
⊢ (↑(∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ) : ℂ) + (↑(∫ (x : F), (L₂ : (a : F) → ℝ) x ∂ν) : ℂ) =
    (↑(∫ (x : E × F), (L : (a : E × F) → ℝ) x ∂μ.prod ν) : ℂ)

Tactic:
rw [integral_continuousLinearMap_prod' (IsGaussian.integrable_dual μ (L.comp (.inl ℝ E F)))
      (IsGaussian.integrable_dual ν (L.comp (.inr ℝ E F)))]

Premises used: ContinuousLinearMap.comp, ProbabilityTheory.IsGaussian.integrable_dual, Real, MeasureTheory.integral_continuousLinearMap_prod', ContinuousLinearMap.inr, ContinuousLinearMap.inl
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
e_z e_z₁ e_z₂ e_z₃ :
  HAdd.hAdd (α := ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ) (∫ (x : F), (L₂ : (a : F) → ℝ) x ∂ν) =
    HAdd.hAdd (α := ℝ)
      (∫ (x : E), (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) x ∂μ)
      (∫ (y : F), (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) y ∂ν)
⊢ (↑(∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ) : ℂ) + (↑(∫ (x : F), (L₂ : (a : F) → ℝ) x ∂ν) : ℂ) =
    (↑(HAdd.hAdd (α := ℝ)
          (∫ (x : E),
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) x ∂μ)
          (∫ (y : F),
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) y ∂ν)) :
      ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
e_z :
  (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) = (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ)
⊢ (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) / 2 + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) / 2 =
    (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2

Tactic:
field_simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
e_z :
  (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) =
    (↑(Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) : (a : E) → ℝ); μ] +
          Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)) : (a : F) → ℝ); ν]) :
      ℂ)
⊢ (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) = (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ)

Tactic:
rw [variance_dual_prod' (IsGaussian.memLp_dual μ (L.comp (.inl ℝ E F)) 2 (by simp))
      (IsGaussian.memLp_dual ν (L.comp (.inr ℝ E F)) 2 (by simp))]

Premises used: ContinuousLinearMap.comp, Real, ProbabilityTheory.IsGaussian.memLp_dual, ContinuousLinearMap.inr, ProbabilityTheory.variance_dual_prod', ContinuousLinearMap.inl, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
hL₁ : L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)
L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
hL₂ : L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)
e_z e_z₁ e_z₂ e_z₃ :
  Var[(⇑L₁ : (a : E) → ℝ); μ] + Var[(⇑L₂ : (a : F) → ℝ); ν] =
    Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) : (a : E) → ℝ); μ] +
      Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)) : (a : F) → ℝ); ν]
⊢ (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) =
    (↑(Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) : (a : E) → ℝ); μ] +
          Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)) : (a : F) → ℝ); ν]) :
      ℂ)

Tactic:
norm_cast
-- 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 : IsGaussian μ
L : StrongDual ℝ E
rw : Integrable id μ
h : MemLp id 2 μ
⊢ charFunDual μ L =
    cexp
      ((↑((L : (a : E) → ℝ) (∫ (x : E), id x ∂μ)) : ℂ) * I -
        (↑((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                  (a : StrongDual ℝ E) → ℝ)
                L) :
            ℂ) /
          2)

Tactic:
rw [IsGaussian.charFunDual_eq, covarianceBilinDual_self_eq_variance, integral_complex_ofReal,
    L.integral_comp_id_comm']

Premises used: ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.covarianceBilinDual_self_eq_variance, ContinuousLinearMap.integral_comp_id_comm', integral_complex_ofReal
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ Integrable id μ

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 : NormedSpace ℝ E
inst_6 : IsGaussian μ
L : StrongDual ℝ E
⊢ Integrable id μ

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 : NormedSpace ℝ E
inst_6 : IsGaussian μ
L : StrongDual ℝ 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 : NormedSpace ℝ E
inst_6 : IsGaussian μ
L : StrongDual ℝ 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 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
⊢ IsGaussian μ ↔
    ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
      f.toBilinForm.IsPosSemidef ∧
        ∀ (L : StrongDual ℝ E),
          charFunDual μ L =
            cexp
              ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
                (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L) :
                    ℂ) /
                  2)

Tactic:
⟨fun h ↦ ⟨μ[id], covarianceBilinDual μ, isPosSemidef_covarianceBilinDual,
    h.charFunDual_eq'⟩,
    fun ⟨m, f, hf, h⟩ ↦ isGaussian_of_map_eq_gaussianReal fun L ↦ ⟨L m, (f L L).toNNReal, ?_⟩⟩

Premises used: ProbabilityTheory.IsGaussian, id, ProbabilityTheory.isGaussian_of_map_eq_gaussianReal, ProbabilityTheory.covarianceBilinDual, ProbabilityTheory.isPosSemidef_covarianceBilinDual, MeasureTheory.integral, And.intro, Iff.intro, Exists.intro, _private.0.ProbabilityTheory.isGaussian_iff_gaussian_charFunDual.match_1, ProbabilityTheory.IsGaussian.charFunDual_eq', DFunLike.coe, Real.toNNReal
-- 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 μ
refine :
  (∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
      f.toBilinForm.IsPosSemidef ∧
        ∀ (L : StrongDual ℝ E),
          charFunDual μ L =
            cexp
              ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
                (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L) :
                    ℂ) /
                  2)) →
    ∀ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (hf : f.toBilinForm.IsPosSemidef)
      (h :
        ∀ (L : StrongDual ℝ E),
          charFunDual μ L =
            cexp
              ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
                (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L) :
                    ℂ) /
                  2))
      (L : E →L[ℝ] ℝ),
      Measure.map (⇑L : (a : E) → ℝ) μ =
        gaussianReal ((L : (a : E) → ℝ) m)
          (Real.toNNReal
            ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                (a : StrongDual ℝ E) → ℝ)
              L))
⊢ IsGaussian μ ↔
    ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
      f.toBilinForm.IsPosSemidef ∧
        ∀ (L : StrongDual ℝ E),
          charFunDual μ L =
            cexp
              ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
                (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                          (a : StrongDual ℝ E) → ℝ)
                        L) :
                    ℂ) /
                  2)

Tactic:
refine ⟨fun h ↦ ⟨μ[id], covarianceBilinDual μ, isPosSemidef_covarianceBilinDual,
    h.charFunDual_eq'⟩,
    fun ⟨m, f, hf, h⟩ ↦ isGaussian_of_map_eq_gaussianReal fun L ↦ ⟨L m, (f L L).toNNReal, ?_⟩⟩
-- 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 μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
h₁ :
  charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) =
    charFun
      (gaussianReal ((L : (a : E) → ℝ) m)
        (Real.toNNReal
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L)))
⊢ Measure.map (⇑L : (a : E) → ℝ) μ =
    gaussianReal ((L : (a : E) → ℝ) m)
      (Real.toNNReal
        ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
          L))

Tactic:
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 : NormedSpace ℝ E
inst_6 : IsFiniteMeasure μ
h_1 :
  ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ),
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ E),
        charFunDual μ L =
          cexp
            ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
              (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                        (a : StrongDual ℝ E) → ℝ)
                      L) :
                  ℂ) /
                2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        ((↑((L : (a : E) → ℝ) m) : ℂ) * I -
          (↑((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                    (a : StrongDual ℝ E) → ℝ)
                  L) :
              ℂ) /
            2)
L : E →L[ℝ] ℝ
h₁ :
  ∀ (t : ℝ),
    charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) t =
      charFun
        (gaussianReal ((L : (a : E) → ℝ) m)
          (Real.toNNReal
            ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
                (a : StrongDual ℝ E) → ℝ)
              L)))
        t
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) =
    charFun
      (gaussianReal ((L : (a : E) → ℝ) m)
        (Real.toNNReal
          ((((f : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ)
            L)))

Tactic:
ext t