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 μ
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) (fun (x : E) ↦ x + c) μ

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
μ : 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 : ℝ)
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := inst_2) (fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ))
    (Measure.map (fun (x : E) ↦ x + c) μ)

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
μ : 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 : ℝ)
⊢ AEStronglyMeasurable (β := ℝ) (⇑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
μ : 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 : ℝ)
rw :
  cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp ((↑(∫ (x : E), (L : (a : E) → ℝ) (x + c) ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
⊢ 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)

Tactic:
rw [variance_map (by fun_prop) (by fun_prop), integral_map (by fun_prop) (by fun_prop),
    hL_comp, variance_add_const (by fun_prop), integral_complex_ofReal, integral_complex_ofReal]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.variance_add_const, ProbabilityTheory.variance_map, 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 μ
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 : ℝ)
simp :
  cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((↑(∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ) ∂μ) : ℂ) * I -
        (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
⊢ cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp ((↑(∫ (x : E), (L : (a : E) → ℝ) (x + c) ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)

Tactic:
simp only [map_add]

Premises used: map_add
-- 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 : ℝ)
⊢ Integrable (ε := ℝ) (⇑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
μ : 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 : ℝ)
funProp : enorm (E := ℝ) ((L : (a : E) → ℝ) c : ℝ) ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (L : (a : E) → ℝ) c) μ

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
μ : 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 : ℝ)
rw :
  cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((↑(HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ) (∫ (a : E), (L : (a : E) → ℝ) c ∂μ)) : ℂ) * I -
        (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
⊢ cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((↑(∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ) ∂μ) : ℂ) * I -
        (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)

Tactic:
rw [integral_add (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_add
-- 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 : ℝ)
e_z :
  (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I =
    (↑(HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ) (∫ (a : E), (L : (a : E) → ℝ) c ∂μ)) : ℂ) * I -
      (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2
⊢ cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((↑(HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ) (∫ (a : E), (L : (a : E) → ℝ) c ∂μ)) : ℂ) * I -
        (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 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 μ
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 : ℝ)
e_z :
  (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I =
    ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) + (↑((L : (a : E) → ℝ) c) : ℂ)) * I -
      (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2
⊢ (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I =
    (↑(HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ) (∫ (a : E), (L : (a : E) → ℝ) c ∂μ)) : ℂ) * I -
      (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2

Tactic:
simp only [integral_const, probReal_univ, smul_eq_mul, one_mul, ofReal_add]

Premises used: Complex.ofReal_add, MeasureTheory.integral_const, MeasureTheory.probReal_univ, smul_eq_mul, one_mul
-- 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 : ℝ)
⊢ (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I =
    ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) + (↑((L : (a : E) → ℝ) c) : ℂ)) * I -
      (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2

Tactic:
ring
-- 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
simp_rw : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ)
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + x) μ)

Tactic:
simp_rw [add_comm c]

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

Tactic:
infer_instance
-- 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
simp_rw : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x + -c) μ)
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x - c) μ)

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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:
infer_instance
-- 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 μ
change : IsGaussian (E := E) (mE := inst_2) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ -x) μ)

Tactic:
change IsGaussian (μ.map (ContinuousLinearEquiv.neg ℝ))

Premises used: ProbabilityTheory.IsGaussian, Real, ContinuousLinearEquiv.neg, MeasureTheory.Measure.map, DFunLike.coe
-- 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 μ
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)

Tactic:
infer_instance
-- 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
simp_rw : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c - x) μ)

Tactic:
simp_rw [sub_eq_add_neg]

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

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
μ : Measure E
inst_8 : IsGaussian μ
c : E
this : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + x) (Measure.map (fun (x : E) ↦ -x) μ))
⊢ Measurable (β := E) fun (x : E) ↦ -x

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
μ : Measure E
inst_8 : IsGaussian μ
c : E
this : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + x) (Measure.map (fun (x : E) ↦ -x) μ))
rwa :
  ∀ (this : IsGaussian (E := E) (mE := inst_2) (Measure.map ((fun (x : E) ↦ c + x) ∘ fun (x : E) ↦ -x) μ)),
    IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)),
    IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)

Tactic:
rwa [Measure.map_map (by fun_prop) (by fun_prop), Function.comp_def] at this

Premises used: Function.comp_def, MeasureTheory.Measure.map_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
μ : Measure E
inst_8 : IsGaussian μ
c : E
suffices : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + x) (Measure.map (fun (x : E) ↦ -x) μ))
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)

Tactic:
suffices IsGaussian ((μ.map (fun x ↦ -x)).map (fun x ↦ c + x)) by
    rwa [Measure.map_map (by fun_prop) (by fun_prop), Function.comp_def] at this
-- 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) ↦ c + x) (Measure.map (fun (x : E) ↦ -x) μ))

Tactic:
infer_instance
-- 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 ν
⊢ IsGaussian (μ.prod ν)

Tactic:
isGaussian_of_charFunDual_eq fun L ↦ ?_

Premises used: setOf, 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 μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
refine :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (μ.prod ν) L =
      cexp
        ((∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν) * I -
          (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2)
⊢ IsGaussian (μ.prod ν)

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 μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
rw :
  cexp
      ((∫ (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)) =
    cexp
      ((∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν) * I -
        (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2)
⊢ charFunDual (μ.prod ν) L =
    cexp
      ((∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν) * I -
        (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2)

Tactic:
rw [charFunDual_prod, IsGaussian.charFunDual_eq, IsGaussian.charFunDual_eq, ← Complex.exp_add]

Premises used: Complex.exp_add, MeasureTheory.charFunDual_prod, ProbabilityTheory.IsGaussian.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 μ
inst_9 : SecondCountableTopologyEither E F
ν : Measure F
inst_10 : IsGaussian ν
L : StrongDual ℝ (E × F)
e_z :
  (∫ (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
⊢ cexp
      ((∫ (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)) =
    cexp
      ((∫ (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)
⊢ let L₁ : E →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F);
  L₁ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)

Tactic:
let (eq := hL₁) L₁ := L.comp (.inl ℝ E F)
-- 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)
⊢ let L₂ : F →L[ℝ] ℝ := ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F);
  L₂ = ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F)

Tactic:
let (eq := hL₂) L₂ := L.comp (.inr ℝ E F)