awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
h₁ :
  cexp ((∫ (x : E), (↑((u • L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑(u • L) : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp
      ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
        (↑(↑Var[(⇑L : (a : E) → ℝ); μ].toNNReal : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u =
    charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) u

Tactic:
rw [charFun_map_eq_charFunDual_smul L u, h (u • L), charFun_gaussianReal]

Premises used: HSMul.hSMul, MeasureTheory.charFun_map_eq_charFunDual_smul, ProbabilityTheory.charFun_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
h₁ :
  cexp
      ((∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I -
        (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp
      ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
        (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)
⊢ cexp ((∫ (x : E), (↑((u • L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑(u • L) : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp
      ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
        (↑(↑Var[(⇑L : (a : E) → ℝ); μ].toNNReal : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)

Tactic:
simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul, ofReal_mul,
    Real.coe_toNNReal']

Premises used: ContinuousLinearMap.coe_smul', Real.coe_toNNReal', smul_eq_mul, Complex.ofReal_mul, Pi.smul_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
h₁ : ∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
h₂ :
  (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) =
    (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2
⊢ cexp
      ((∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I -
        (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp
      ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
        (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
h₁ : (↑u : ℂ) * ∫ (a : E), (↑((L : (a : E) → ℝ) a) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
h₂ h₃ : (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
⊢ ∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)

Tactic:
rw [integral_const_mul, integral_complex_ofReal]

Premises used: MeasureTheory.integral_const_mul, integral_complex_ofReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
h₁ :
  (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) =
    (↑Var[fun (ω : E) ↦ HMul.hMul (β := ℝ) u ((L : (a : E) → ℝ) ω : ℝ); μ] : ℂ)
⊢ (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) =
    (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2

Tactic:
rw [max_eq_left (variance_nonneg _ _), mul_comm, ← ofReal_pow, ← ofReal_mul,
      ← variance_const_mul]

Premises used: max_eq_left, ProbabilityTheory.variance_nonneg, mul_comm, Complex.ofReal_pow, ProbabilityTheory.variance_const_mul, Complex.ofReal_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
⊢ (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) =
    (↑Var[fun (ω : E) ↦ HMul.hMul (β := ℝ) u ((L : (a : E) → ℝ) ω : ℝ); μ] : ℂ)

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
t : E
rw :
  cexp
      ((∫ (x : E), (↑((((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t : StrongDual ℝ E) : (a : E) → ℝ) x) : ℂ) ∂μ) * I -
        (↑Var[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t : StrongDual ℝ E) : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp ((∫ (x : E), (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)
⊢ charFun μ t = cexp ((∫ (x : E), (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)

Tactic:
rw [charFun_eq_charFunDual_toDualMap, IsGaussian.charFunDual_eq]

Premises used: ProbabilityTheory.IsGaussian.charFunDual_eq, MeasureTheory.charFun_eq_charFunDual_toDualMap
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
t : E
⊢ cexp
      ((∫ (x : E), (↑((((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t : StrongDual ℝ E) : (a : E) → ℝ) x) : ℂ) ∂μ) * I -
        (↑Var[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t : StrongDual ℝ E) : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp ((∫ (x : E), (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)

Tactic:
simp [toDualMap]

Premises used: InnerProductSpace.toDualMap
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsFiniteMeasure μ
simp_rw :
  (∀ (x : E),
      charFunDual μ ((toDual ℝ E : (a : E) → StrongDual ℝ E) x) =
        cexp
          ((∫ (x_1 : E), (↑((((toDual ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ) x_1) : ℂ) ∂μ) *
              I -
            (↑Var[(⇑((toDual ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ); μ] : ℂ) / 2)) ↔
    ∀ (t : E),
      charFunDual μ ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t) =
        cexp ((∫ (x : E), (↑⟪t, x⟫ : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)
⊢ IsGaussian μ ↔
    ∀ (t : E),
      charFun μ t =
        cexp ((∫ (x : E), (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)

Tactic:
simp_rw [isGaussian_iff_charFunDual_eq, (toDual ℝ E).surjective.forall,
    charFun_eq_charFunDual_toDualMap]

Premises used: LinearIsometryEquiv.surjective, InnerProductSpace.toDual, Real, Function.Surjective.forall, ProbabilityTheory.isGaussian_iff_charFunDual_eq, MeasureTheory.charFun_eq_charFunDual_toDualMap
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsFiniteMeasure μ
⊢ (∀ (x : E),
      charFunDual μ ((toDual ℝ E : (a : E) → StrongDual ℝ E) x) =
        cexp
          ((∫ (x_1 : E), (↑((((toDual ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ) x_1) : ℂ) ∂μ) *
              I -
            (↑Var[(⇑((toDual ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ); μ] : ℂ) / 2)) ↔
    ∀ (t : E),
      charFunDual μ ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t) =
        cexp ((∫ (x : E), (↑⟪t, x⟫ : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)

Tactic:
simp [toDualMap, toDual]

Premises used: InnerProductSpace.toDual, InnerProductSpace.toDualMap
-- 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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
⊢ AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) (μ ∗ ν)

Tactic:
fun_prop
-- 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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ x) (Measure.map (⇑L : (a : E) → ℝ) (μ ∗ ν))

Tactic:
fun_prop
-- 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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
rw :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) (μ ∗ ν)) fun (x : ℝ) ↦ x)
rw₁ rw₂ : Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
⊢ Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)

Tactic:
rw [← Measure.map_conv_continuousLinearMap L,
        integral_map (φ := L) (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map, MeasureTheory.Measure.map_conv_continuousLinearMap
-- 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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
⊢ Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)

Tactic:
have : (μ ∗ ν)[L] = ∫ x, x ∂((μ.map L).conv (ν.map L)) := by
      rw [← Measure.map_conv_continuousLinearMap L,
        integral_map (φ := L) (by fun_prop) (by fun_prop)]
-- 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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
this :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
⊢ AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) (μ ∗ ν)

Tactic:
fun_prop
-- 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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
this :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
rw :
  gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
      (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal) =
    gaussianReal
      (∫ (x : ℝ),
        x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
          (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal))
      Var[id;
          gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
            (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)].toNNReal
⊢ Measure.map (⇑L : (a : E) → ℝ) (μ ∗ ν) =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν) Var[(⇑L : (a : E) → ℝ); μ ∗ ν].toNNReal

Tactic:
rw [Measure.map_conv_continuousLinearMap L, this, ← variance_id_map (by fun_prop),
      Measure.map_conv_continuousLinearMap L, IsGaussian.map_eq_gaussianReal L,
      IsGaussian.map_eq_gaussianReal L, gaussianReal_conv_gaussianReal]

Premises used: ProbabilityTheory.IsGaussian.map_eq_gaussianReal, ProbabilityTheory.gaussianReal_conv_gaussianReal, MeasureTheory.Measure.map_conv_continuousLinearMap, ProbabilityTheory.variance_id_map
-- 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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
this :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
e_μ :
  HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν) =
    ∫ (x : ℝ),
      x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
        (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)
e_v :
  Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal =
    Var[id;
        gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
          (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)].toNNReal
⊢ gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
      (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal) =
    gaussianReal
      (∫ (x : ℝ),
        x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
          (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal))
      Var[id;
          gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
            (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)].toNNReal

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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
this :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
⊢ HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν) =
    ∫ (x : ℝ),
      x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
        (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)

Tactic:
simp [variance_nonneg]

Premises used: ProbabilityTheory.variance_nonneg
-- 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
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
this :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
⊢ Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal =
    Var[id;
        gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
          (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)].toNNReal

Tactic:
simp [variance_nonneg]

Premises used: ProbabilityTheory.variance_nonneg
-- 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 μ
c : E
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ)

Tactic:
isGaussian_of_charFunDual_eq fun L ↦ ?_

Premises used: ProbabilityTheory.isGaussian_of_charFunDual_eq
-- 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 μ
c : E
refine :
  ∀ (L : StrongDual ℝ E),
    charFunDual (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ) L =
      cexp
        ((@integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ x + c) μ) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) *
            I -
          (↑(variance (Ω := E) (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)) : ℂ) / 2)
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ)

Tactic:
refine isGaussian_of_charFunDual_eq fun L ↦ ?_

Premises used: ProbabilityTheory.isGaussian_of_charFunDual_eq
-- 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 μ
c : E
L : StrongDual ℝ E
rw :
  cexp
      ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((@integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ x + c) μ) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (Ω := E) (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)) : ℂ) / 2)
⊢ charFunDual (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ) L =
    cexp
      ((@integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ x + c) μ) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (Ω := E) (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)) : ℂ) / 2)

Tactic:
rw [charFunDual_map_add_const, IsGaussian.charFunDual_eq, ← exp_add]

Premises used: Complex.exp_add, ProbabilityTheory.IsGaussian.charFunDual_eq, MeasureTheory.charFunDual_map_add_const
-- 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 μ
c : E
L : StrongDual ℝ E
h :
  ∀ (x : E),
    Function.comp (β := E) (⇑L : (a : E) → ℝ) (fun (x : E) ↦ x + c) x =
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
⊢ Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)

Tactic:
ext
-- 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 μ
c : E
L : StrongDual ℝ E
x : E
⊢ Function.comp (β := E) (⇑L : (a : E) → ℝ) (fun (x : E) ↦ x + c) x =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)

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 μ
c : E
L : StrongDual ℝ E
⊢ Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)

Tactic:
have hL_comp : L ∘ (fun x ↦ x + c) = fun x ↦ L x + L c := by ext; 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 μ
c : E
L : StrongDual ℝ E
hL_comp :
  Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
⊢ AEMeasurable (α := E) (β := ℝ) (_m := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)

Tactic:
fun_prop