awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
h :
  ∀ (L : StrongDual ℝ (E × E)),
    charFunDual (mE := Prod.instMeasurableSpace)
        (Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ)) L =
      charFunDual (μ.prod μ) L
⊢ Eq (α := (L : StrongDual ℝ (E × E)) → ℂ)
    (charFunDual (mE := Prod.instMeasurableSpace)
      (Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ)))
    (charFunDual (μ.prod μ))

Tactic:
ext L
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h :
  cexp
      (-(↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) /
          2 +
        -(↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inr ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) /
          2) =
    cexp
      (-(↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) /
          2 +
        -(↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) /
          2)
⊢ charFunDual (mE := Prod.instMeasurableSpace)
      (Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ)) L =
    charFunDual (μ.prod μ) L

Tactic:
simp_rw [charFunDual_map, charFunDual_prod, charFunDual_eq_of_forall_strongDual_eq_zero hμ,
    ← Complex.exp_add]

Premises used: Complex.exp_add, MeasureTheory.charFunDual_prod, ProbabilityTheory.IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero, MeasureTheory.charFunDual_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h :
  cexp
      (-((↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) +
            (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ)
                        (ContinuousLinearMap.inr ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ)) /
        2) =
    cexp
      (-((↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) +
            (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
                  μ] :
              ℂ)) /
        2)
⊢ cexp
      (-(↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) /
          2 +
        -(↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inr ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) /
          2) =
    cexp
      (-(↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) /
          2 +
        -(↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) /
          2)

Tactic:
rw [← add_div, ← add_div, ← neg_add, ← neg_add]

Premises used: neg_add, add_div
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h :
  (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
              (a : E) → ℝ);
            μ] :
        ℂ) +
      (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inr ℝ E E)) :
              (a : E) → ℝ);
            μ] :
        ℂ) =
    (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] : ℂ) +
      (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ] : ℂ)
⊢ cexp
      (-((↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ) +
            (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ)
                        (ContinuousLinearMap.inr ℝ E E)) :
                    (a : E) → ℝ);
                  μ] :
              ℂ)) /
        2) =
    cexp
      (-((↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] :
              ℂ) +
            (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
                  μ] :
              ℂ)) /
        2)

Tactic:
congr 3
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h :
  Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
          (a : E) → ℝ);
        μ] +
      Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inr ℝ E E)) :
          (a : E) → ℝ);
        μ] =
    Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] +
      Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ]
⊢ (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inl ℝ E E)) :
              (a : E) → ℝ);
            μ] :
        ℂ) +
      (↑Var[(⇑((L ∘SL ContinuousLinearMap.rotation θ).comp (σ₁₂ := RingHom.id ℝ) (ContinuousLinearMap.inr ℝ E E)) :
              (a : E) → ℝ);
            μ] :
        ℂ) =
    (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ); μ] : ℂ) +
      (↑Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ] : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h :
  ∀ (x : E),
    Eq (α := ℝ) (((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E : (a : E) → ℝ) x : ℝ)
      ((HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
              HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) :
            (a : E) → ℝ)
          x :
        ℝ)
⊢ (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))

Tactic:
ext x
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
x : E
h :
  Eq (α := ℝ) ((L : (a : E × E) → ℝ) (Real.cos θ • x, -Real.sin θ • x) : ℝ)
    ((HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
            HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) :
          (a : E) → ℝ)
        x :
      ℝ)
⊢ Eq (α := ℝ) (((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E : (a : E) → ℝ) x : ℝ)
    ((HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
            HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) :
          (a : E) → ℝ)
        x :
      ℝ)

Tactic:
simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inl_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, add_zero]

Premises used: ContinuousLinearMap.coe_comp', smul_zero, ContinuousLinearMap.rotation_apply, ContinuousLinearMap.inl_apply, Function.comp_apply, add_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
x : E
h :
  HAdd.hAdd (α := ℝ) (β := ℝ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E) : (a : E) → ℝ)
          (Real.cos θ • x, -Real.sin θ • x).1 :
        ℝ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E) : (a : E) → ℝ)
          (Real.cos θ • x, -Real.sin θ • x).2 :
        ℝ) =
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
          HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) :
        (a : E) → ℝ)
      x
⊢ Eq (α := ℝ) ((L : (a : E × E) → ℝ) (Real.cos θ • x, -Real.sin θ • x) : ℝ)
    ((HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
            HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) :
          (a : E) → ℝ)
        x :
      ℝ)

Tactic:
rw [← L.comp_inl_add_comp_inr]

Premises used: ContinuousLinearMap.comp_inl_add_comp_inr
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
x : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E) : (a : E) → ℝ)
          (Real.cos θ • x, -Real.sin θ • x).1 :
        ℝ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E) : (a : E) → ℝ)
          (Real.cos θ • x, -Real.sin θ • x).2 :
        ℝ) =
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
          HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) :
        (a : E) → ℝ)
      x

Tactic:
simp [-neg_smul, sub_eq_add_neg]

Premises used: neg_smul, sub_eq_add_neg
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))

Tactic:
have h1 : (L.comp (.rotation θ)).comp (.inl ℝ E E)
      = Real.cos θ • L.comp (.inl ℝ E E) - Real.sin θ • L.comp (.inr ℝ E E) := by
    ext x
    simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inl_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, add_zero]
    rw [← L.comp_inl_add_comp_inr]
    simp [-neg_smul, sub_eq_add_neg]
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))
h :
  ∀ (x : E),
    Eq (α := ℝ) (((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E : (a : E) → ℝ) x : ℝ)
      ((HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) +
              HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) :
            (a : E) → ℝ)
          x :
        ℝ)
⊢ (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) +
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))

Tactic:
ext x
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))
x : E
h :
  (L : (a : E × E) → ℝ) (Real.sin θ • x, Real.cos θ • x) =
    HMul.hMul (β := ℝ) (Real.sin θ) ((L : (a : E × E) → ℝ) (x, 0) : ℝ) +
      HMul.hMul (β := ℝ) (Real.cos θ) ((L : (a : E × E) → ℝ) (0, x) : ℝ)
⊢ Eq (α := ℝ) (((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E : (a : E) → ℝ) x : ℝ)
    ((HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) +
            HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) :
          (a : E) → ℝ)
        x :
      ℝ)

Tactic:
simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inr_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, zero_add, ContinuousLinearMap.add_apply,
      ContinuousLinearMap.coe_smul', Pi.smul_apply, ContinuousLinearMap.inl_apply, smul_eq_mul]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_smul', smul_zero, ContinuousLinearMap.add_apply, zero_add, ContinuousLinearMap.inr_apply, ContinuousLinearMap.rotation_apply, ContinuousLinearMap.inl_apply, Function.comp_apply, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))
x : E
h :
  HAdd.hAdd (α := ℝ) (β := ℝ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E) : (a : E) → ℝ)
          (Real.sin θ • x, Real.cos θ • x).1 :
        ℝ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E) : (a : E) → ℝ)
          (Real.sin θ • x, Real.cos θ • x).2 :
        ℝ) =
    HMul.hMul (β := ℝ) (Real.sin θ) ((L : (a : E × E) → ℝ) (x, 0) : ℝ) +
      HMul.hMul (β := ℝ) (Real.cos θ) ((L : (a : E × E) → ℝ) (0, x) : ℝ)
⊢ (L : (a : E × E) → ℝ) (Real.sin θ • x, Real.cos θ • x) =
    HMul.hMul (β := ℝ) (Real.sin θ) ((L : (a : E × E) → ℝ) (x, 0) : ℝ) +
      HMul.hMul (β := ℝ) (Real.cos θ) ((L : (a : E × E) → ℝ) (0, x) : ℝ)

Tactic:
rw [← L.comp_inl_add_comp_inr]

Premises used: ContinuousLinearMap.comp_inl_add_comp_inr
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))
x : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E) : (a : E) → ℝ)
          (Real.sin θ • x, Real.cos θ • x).1 :
        ℝ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E) : (a : E) → ℝ)
          (Real.sin θ • x, Real.cos θ • x).2 :
        ℝ) =
    HMul.hMul (β := ℝ) (Real.sin θ) ((L : (a : E × E) → ℝ) (x, 0) : ℝ) +
      HMul.hMul (β := ℝ) (Real.cos θ) ((L : (a : E × E) → ℝ) (0, x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
inst_6 : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) -
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))
⊢ (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sin θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) +
      HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos θ)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E))

Tactic:
have h2 : (L.comp (.rotation θ)).comp (.inr ℝ E E)
      = Real.sin θ • L.comp (.inl ℝ E E) + Real.cos θ • L.comp (.inr ℝ E E) := by
    ext x
    simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inr_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, zero_add, ContinuousLinearMap.add_apply,
      ContinuousLinearMap.coe_smul', Pi.smul_apply, ContinuousLinearMap.inl_apply, smul_eq_mul]
    rw [← L.comp_inl_add_comp_inr]
    simp