awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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 (fun (x : E) ↦ -x) μ)
have change : IsGaussian (E := E) (mE := inst_2) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
Tactic: change IsGaussian (μ.map (ContinuousLinearEquiv.neg ℝ))
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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) μ)
have simp_rw : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)
Tactic: simp_rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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) μ))
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)
have 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) μ)
Tactic: rwa [Measure.map_map (by fun_prop) (by fun_prop), Function.comp_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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) μ)
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + -x) μ)
have 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) μ)
Tactic: rwa [Measure.map_map (by fun_prop) (by fun_prop), Function.comp_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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) μ)
have suffices : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + x) (Measure.map (fun (x : E) ↦ -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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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 ν)
have 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)
Tactic: refine isGaussian_of_charFunDual_eq fun L ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ charFunDual (μ.prod ν) L =
    cexp
      ((∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν) * I -
        (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2)
have 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)
Tactic: rw [charFunDual_prod, IsGaussian.charFunDual_eq, IsGaussian.charFunDual_eq, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ 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)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (hypothesis)
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)
⊢ (∫ (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
have hL₁ : 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)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (hypothesis)
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)
⊢ (∫ (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
have hL₂ : 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)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ (∫ (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
have 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
Tactic: rw [← hL₁, ← hL₂, sub_add_sub_comm, ← add_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ 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
have 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 ν
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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 ν
⊢ 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
have e_z₁ : (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) / 2 + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) / 2 =
  (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ HAdd.hAdd (α := ℂ) (∫ (x : E), (↑((L₁ : (a : E) → ℝ) x) : ℂ) ∂μ) (∫ (x : F), (↑((L₂ : (a : F) → ℝ) x) : ℂ) ∂ν) =
    ∫ (x : E × F), (↑((L : (a : E × F) → ℝ) x) : ℂ) ∂μ.prod ν
have e_z : (↑(∫ (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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ (↑(∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ) : ℂ) + (↑(∫ (x : F), (L₂ : (a : F) → ℝ) x ∂ν) : ℂ) =
    (↑(∫ (x : E × F), (L : (a : E × F) → ℝ) x ∂μ.prod ν) : ℂ)
have 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 ∂ν)) :
    ℂ)
Tactic: rw [integral_continuousLinearMap_prod' (IsGaussian.integrable_dual μ (L.comp (.inl ℝ E F)))
      (IsGaussian.integrable_dual ν (L.comp (.inr ℝ E F)))]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ (↑(∫ (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 ∂ν)) :
      ℂ)
have 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 ∂ν)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) / 2 + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) / 2 =
    (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ) / 2
have e_z : (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) = (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
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)
⊢ (↑Var[(⇑L₁ : (a : E) → ℝ); μ] : ℂ) + (↑Var[(⇑L₂ : (a : F) → ℝ); ν] : ℂ) = (↑Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] : ℂ)
have 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) → ℝ); ν]) :
    ℂ)
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))]