awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ @Integrable _ _ _ _ inst_1 id (Measure.map X P)

Tactic:
hX.isGaussian_map.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ @Integrable _ _ _ _ inst_1 id (Measure.map X P)

Tactic:
exact hX.isGaussian_map.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
e_a :
  cexp
      ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F) : (a : F) → ℝ)
                (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (x : F) ↦ x)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_6) (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ)
                (Measure.map Y P)) :
            ℂ) /
          2) =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_6) (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ)
                (Measure.map Y P)) :
            ℂ) /
          2)
e_a₁ : MemLp (m0 := inst_6) id 2 (Measure.map Y P)
e_a₂ : @Integrable _ _ _ _ inst_6 id (Measure.map Y P)
⊢ charFunDual (mE := inst_6) (Measure.map Y P) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)) :
            ℂ) *
          I -
        (↑((((covarianceBilinDual (mE := inst_6) (Measure.map Y P) : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ)
                      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) :
                    StrongDual ℝ F →L[ℝ] ℝ) :
                  (a : StrongDual ℝ F) → ℝ)
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))) :
            ℂ) /
          2)

Tactic:
rw [hY.isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
        covarianceBilinDual_self_eq_variance]

Premises used: ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.covarianceBilinDual_self_eq_variance, integral_complex_ofReal, ContinuousLinearMap.integral_comp_id_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ cexp
      ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F) : (a : F) → ℝ)
                (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (x : F) ↦ x)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_6) (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ)
                (Measure.map Y P)) :
            ℂ) /
          2) =
    cexp
      ((↑((L : (a : E × F) → ℝ)
                ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)) :
            ℂ) *
          I -
        (↑(variance (mΩ := inst_6) (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ)
                (Measure.map Y P)) :
            ℂ) /
          2)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ MemLp (m0 := inst_6) id 2 (Measure.map Y P)

Tactic:
hY.isGaussian_map.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ MemLp (m0 := inst_6) id 2 (Measure.map Y P)

Tactic:
exact hY.isGaussian_map.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ @Integrable _ _ _ _ inst_6 id (Measure.map Y P)

Tactic:
hY.isGaussian_map.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x,
      @integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) =
    HAdd.hAdd (α := E × F) (β := E × F)
      ((inl ℝ E F : (a : E) → E × F) (@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ x) : E × F)
      ((inr ℝ E F : (a : F) → E × F) (@integral _ _ _ _ inst_6 (Measure.map Y P) fun (y : F) ↦ y) : E × F)
⊢ @Integrable _ _ _ _ inst_6 id (Measure.map Y P)

Tactic:
exact hY.isGaussian_map.integrable_id

Premises used: ProbabilityTheory.IsGaussian.integrable_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
⊢ IsProbabilityMeasure P

Tactic:
have := hXY.isProbabilityMeasure
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this : IsProbabilityMeasure P
rw :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
      charFunDual (mE := inst_1) (Measure.map X P) (comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
        charFunDual (mE := inst_6) (Measure.map Y P) (comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))
⊢ X ⟂ᵢ[P] Y

Tactic:
rw [indepFun_iff_charFunDual_prod hXY.fst.aemeasurable hXY.snd.aemeasurable]

Premises used: ProbabilityTheory.HasGaussianLaw.snd, ProbabilityTheory.HasGaussianLaw.fst, ProbabilityTheory.HasGaussianLaw.aemeasurable, ProbabilityTheory.indepFun_iff_charFunDual_prod
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
h₁ :
  ∀ (x : Ω),
    Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) (fun (ω : Ω) ↦ (X ω, Y ω)) x =
      HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
        ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) x
⊢ (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
x : Ω
⊢ Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) (fun (ω : Ω) ↦ (X ω, Y ω)) x =
    HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) x

Tactic:
simp [-coe_comp', ← comp_inl_add_comp_inr]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.comp_inl_add_comp_inr
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
⊢ (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)

Tactic:
have : L ∘ (fun ω ↦ (X ω, Y ω)) = (L ∘L (.inl ℝ E F)) ∘ X + (L ∘L (.inr ℝ E F)) ∘ Y := by
    ext; simp [-coe_comp', ← comp_inl_add_comp_inr]
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
rw :
  cexp
      ((↑(∫ (x : Ω),
                HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
                  ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) x ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2) =
    cexp
      ((↑(∫ (a : Ω),
                HAdd.hAdd (α := ℝ) (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) a)
                  (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) a) ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2)
hX : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) 2 P
hY : MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) 2 P
hf : Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) P
hg : Integrable (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) P
⊢ charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
    charFunDual (mE := inst_1) (Measure.map X P) (comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) *
      charFunDual (mE := inst_6) (Measure.map Y P) (comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F))

Tactic:
rw [hXY.charFunDual_map_eq, hXY.fst.charFunDual_map_eq, hXY.snd.charFunDual_map_eq, ← exp_add,
    sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add, this,
    variance_add, h, mul_zero, add_zero]

Premises used: add_mul, Complex.exp_add, Complex.ofReal_add, sub_add_sub_comm, MulZeroClass.mul_zero, ProbabilityTheory.variance_add, ProbabilityTheory.HasGaussianLaw.snd, ProbabilityTheory.HasGaussianLaw.fst, add_zero, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq, MeasureTheory.integral_add, add_div
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ cexp
      ((↑(∫ (x : Ω),
                HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
                  ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) x ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2) =
    cexp
      ((↑(∫ (a : Ω),
                HAdd.hAdd (α := ℝ) (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) a)
                  (((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y) a) ∂P) :
            ℂ) *
          I -
        (↑(Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X; P] +
                Var[(⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y; P]) :
            ℂ) /
          2)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : CompleteSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : NormedAddCommGroup F
inst_6 : MeasurableSpace F
inst_7 : CompleteSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : NormedSpace ℝ E
inst_11 : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (E := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[(⇑L₁ : (a : E) → ℝ) ∘ X, (⇑L₂ : (a : F) → ℝ) ∘ Y; P] = 0
this_1 : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (Function.comp (β := E × F) (⇑L : (a : E × F) → ℝ) fun (ω : Ω) ↦ (X ω, Y ω)) =
    HAdd.hAdd (α := Ω → ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X)
      ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inr ℝ E F)) : (a : F) → ℝ) ∘ Y)
⊢ MemLp (ε := ℝ) ((⇑(comp (σ₁₂ := RingHom.id ℝ) L (inl ℝ E F)) : (a : E) → ℝ) ∘ X) 2 P

Tactic:
(hXY.fst.map _).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.fst, ProbabilityTheory.HasGaussianLaw.memLp_two