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
θ : ℝ
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))
h2 :
  (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))
h :
  Var[(⇑(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) → ℝ);
        μ] +
      Var[(⇑(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) → ℝ);
        μ] =
    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:
rw [h1, h2]
-- 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))
h2 :
  (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))
h :
  Var[HSMul.hSMul (β := (a : E) → ℝ) (Real.cos θ)
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ) -
          HSMul.hSMul (β := (a : E) → ℝ) (Real.sin θ)
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
        μ] +
      Var[HSMul.hSMul (β := (a : E) → ℝ) (Real.sin θ)
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ) +
          HSMul.hSMul (β := (a : E) → ℝ) (Real.cos θ)
            (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (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[(⇑(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) → ℝ);
        μ] +
      Var[(⇑(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) → ℝ);
        μ] =
    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:
simp only [ContinuousLinearMap.coe_sub', ContinuousLinearMap.coe_smul',
    ContinuousLinearMap.coe_add']

Premises used: ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_add', ContinuousLinearMap.coe_sub'
-- 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))
h2 :
  (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))
⊢ HPow.hPow (β := ℕ) (Real.cos θ) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 = 1

Tactic:
have h := Real.cos_sq_add_sin_sq θ
-- 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))
h2 :
  (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))
h : HPow.hPow (β := ℕ) (Real.cos θ) 2 + HPow.hPow (β := ℕ) (Real.sin θ) 2 = 1
⊢ HPow.hPow (β := ℕ) (Real.cos θ) 2 *
            Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ);
              μ] -
          2 *
            (Real.cos θ *
              (Real.sin θ *
                cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ),
                  (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
                  μ])) +
        HPow.hPow (β := ℕ) (Real.sin θ) 2 *
          Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ); μ] +
      (HPow.hPow (β := ℕ) (Real.sin θ) 2 *
            Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ);
              μ] +
          2 *
            (Real.sin θ *
              (Real.cos θ *
                cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ),
                  (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ);
                  μ])) +
        HPow.hPow (β := ℕ) (Real.cos θ) 2 *
          Var[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (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:
grind
-- 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))
h2 :
  (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))
⊢ Ne (α := ℝ≥0∞) 2 ∞

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))
h2 :
  (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))
⊢ MemLp
    (HSMul.hSMul (β := (a : E) → ℝ) (Real.sin θ)
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ))
    2 μ

Tactic:
exact (memLp_dual _ _ _ (by simp)).const_smul _

Premises used: MeasureTheory.MemLp.const_smul, ProbabilityTheory.IsGaussian.memLp_dual
-- 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))
h2 :
  (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))
⊢ MemLp
    (HSMul.hSMul (β := (a : E) → ℝ) (Real.cos θ)
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ))
    2 μ

Tactic:
exact (memLp_dual _ _ _ (by simp)).const_smul _

Premises used: MeasureTheory.MemLp.const_smul, ProbabilityTheory.IsGaussian.memLp_dual
-- 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))
h2 :
  (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))
⊢ MemLp
    (HSMul.hSMul (β := (a : E) → ℝ) (Real.cos θ)
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E E)) : (a : E) → ℝ))
    2 μ

Tactic:
exact (memLp_dual _ _ _ (by simp)).const_smul _

Premises used: MeasureTheory.MemLp.const_smul, ProbabilityTheory.IsGaussian.memLp_dual
-- 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))
h2 :
  (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))
⊢ MemLp
    (HSMul.hSMul (β := (a : E) → ℝ) (Real.sin θ)
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E E)) : (a : E) → ℝ))
    2 μ

Tactic:
exact (memLp_dual _ _ _ (by simp)).const_smul _

Premises used: MeasureTheory.MemLp.const_smul, ProbabilityTheory.IsGaussian.memLp_dual
-- 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
L : StrongDual ℝ E
⊢ Integrable (ε := ℝ) (⇑L : (a : E) → ℝ) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)

Tactic:
fun_prop
-- 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
L : StrongDual ℝ E
rw :
  Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) (x + y) ∂μ)
    0
⊢ Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) 0

Tactic:
rw [integral_conv (by fun_prop)]

Premises used: MeasureTheory.integral_conv
-- 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
L : StrongDual ℝ E
simp :
  Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    0
⊢ Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) (x + y) ∂μ)
    0

Tactic:
simp only [map_add]

Premises used: map_add
-- 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
L : StrongDual ℝ E
e_f :
  ∀ (x : E),
    (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ)) =
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ)
⊢ Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    (∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ)

Tactic:
congr with 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
L : StrongDual ℝ E
x : E
funProp : enorm (E := ℝ) ((L : (a : E) → ℝ) x : ℝ) ≠ ∞
⊢ @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ (L : (a : E) → ℝ) x)
    (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)

Tactic:
fun_prop
-- 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
L : StrongDual ℝ E
x : E
⊢ @Integrable ℝ _ _ E inst_2 (⇑L : (a : E) → ℝ) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)

Tactic:
fun_prop
-- 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
L : StrongDual ℝ E
x : E
e_f :
  HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (a : E) ↦
        (L : (a : E) → ℝ) x)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (a : E) ↦
        (L : (a : E) → ℝ) a) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y :
        ℝ)
⊢ (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y :
        ℝ)

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

Premises used: MeasureTheory.integral_add
-- 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
L : StrongDual ℝ E
x : E
⊢ HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (a : E) ↦
        (L : (a : E) → ℝ) x)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (a : E) ↦
        (L : (a : E) → ℝ) a) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y :
        ℝ)

Tactic:
simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]

Premises used: ContinuousLinearEquiv.coe_neg, MeasureTheory.integral_const, smul_eq_mul
-- 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
L : StrongDual ℝ E
⊢ Integrable (ε := ℝ) (⇑L : (a : E) → ℝ) μ

Tactic:
fun_prop
-- 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
L : StrongDual ℝ E
funProp :
  enorm (E := ℝ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y) ≠
    ∞
⊢ Integrable (ε := ℝ)
    (fun (x : E) ↦
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y)
    μ

Tactic:
fun_prop