mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
h1 : (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) = ∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k
h2 : (⇑L₂ ∘ fun ω k ↦ X (↑j) (↑k) ω) = ∑ k, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑j ↑k
x✝³ : ↥(J i)
x✝² : x✝³ ∈ univ
x✝¹ : ↥(J j)
x✝ : x✝¹ ∈ univ
⊢ ↑i ≠ ↑j

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: case refine_2.hX
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
h1 : (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) = ∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k
h2 : (⇑L₂ ∘ fun ω k ↦ X (↑j) (↑k) ω) = ∑ k, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑j ↑k
⊢ ∀ (i_1 : ↥(J i)), MemLp (⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) i_1) ∘ X ↑i ↑i_1) 2 P

Tactic:
exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨i, k⟩).map _).memLp_two

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
this : μ Set.univ ≤ 2⁻¹
⊢ False

Tactic:
simp at this

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
hi : i ≠ 0
⊢ i.pred hi ≤ j.pred ⋯

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case mp
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint (fun p ↦ f p.2) ((), a) → IsRatStieltjesPoint f a

Tactic:
exact fun h ↦ ⟨h.mono, h.tendsto_atTop_one, h.tendsto_atBot_zero, h.iInf_rat_gt_eq⟩

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case mpr
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint f a → IsRatStieltjesPoint (fun p ↦ f p.2) ((), a)

Tactic:
exact fun h ↦ ⟨h.mono, h.tendsto_atTop_one, h.tendsto_atBot_zero, h.iInf_rat_gt_eq⟩

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : (fun ω i ↦ X i ω) ⟂ᵢ[P] Y
h2 : ∀ (i : S), X i =ᵐ[P] X' i
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : Y ⟂ᵢ[P] fun ω i ↦ X i ω
h2 : ∀ (i : S), X i =ᵐ[P] X' i
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : T → Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : (j : T) → MeasurableSpace (𝓨 j)
X X' : (i : S) → Ω → 𝓧 i
Y Y' : (j : T) → Ω → 𝓨 j
hXY : (fun ω i ↦ X i ω) ⟂ᵢ[P] fun ω j ↦ Y j ω
hX : ∀ (i : S), X i =ᵐ[P] X' i
hY : ∀ (j : T), Y j =ᵐ[P] Y' j
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : T → Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : (j : T) → MeasurableSpace (𝓨 j)
X X' : (i : S) → Ω → 𝓧 i
Y Y' : (j : T) → Ω → 𝓨 j
hXY : (fun ω i ↦ X i ω) ⟂ᵢ[P] fun ω j ↦ Y j ω
hX : ∀ (i : S), X i =ᵐ[P] X' i
hY : ∀ (j : T), Y j =ᵐ[P] Y' j
⊢ ∀ (j : T), ∀ᵐ (a : Unit) ∂Measure.dirac (), Y j =ᵐ[(Kernel.const Unit P) a] Y' j

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos.refine_1.hc
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ ↑⟨q, htq⟩ < 0

Tactic:
Subtype.coe_mk

Goal state after:
case pos.refine_1.hc
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ q < 0
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) P
hY : AEMeasurable Y P
h : ∀ (I : Finset S), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] Y
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (X i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) P
hY : AEMeasurable Y P
h : ∀ (I : Finset S), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] Y
inst✝ : IsZeroOrProbabilityMeasure P
⊢ AEMeasurable Y (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
inst✝² : MeasurableSpace 𝓧
inst✝¹ : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable X P
hY : ∀ (i : S), AEMeasurable (Y i) P
h : ∀ (I : Finset S), X ⟂ᵢ[P] fun ω i ↦ Y (↑i) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ AEMeasurable X (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
inst✝² : MeasurableSpace 𝓧
inst✝¹ : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable X P
hY : ∀ (i : S), AEMeasurable (Y i) P
h : ∀ (I : Finset S), X ⟂ᵢ[P] fun ω i ↦ Y (↑i) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (Y i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) P
hY : ∀ (j : T), AEMeasurable (Y j) P
h : ∀ (I : Finset S) (J : Finset T), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] fun ω j ↦ Y (↑j) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (X i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) P
hY : ∀ (j : T), AEMeasurable (Y j) P
h : ∀ (I : Finset S) (J : Finset T), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] fun ω j ↦ Y (↑j) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (j : T), AEMeasurable (Y j) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : S → Type u_4
𝓧 : (i : S) → T i → Type u_5
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) P
h2 : ∀ (i : S) (j : T i), X i j =ᵐ[P] X' i j
⊢ ∀ (i : S) (j : T i), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i j =ᵐ[(Kernel.const Unit P) a] X' i j

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : S → Type u_4
𝓧 : (i : S) → T i → Type u_5
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) P
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) P
⊢ ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ ⨅ q, f a ↑q

Tactic:
exact le_ciInf fun r' ↦ hf.nonneg a _

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
ω : Ω
⊢ (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)

Tactic:
simp [← map_sum, LinearMap.sum_single_apply]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝² : IsProbabilityMeasure P
this✝¹ : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
this✝ : (i : ι) → Fintype (κ i) := fun i ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 (κ i → ℝ)
y : WithLp 2 (κ j → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ i_1, ((EuclideanSpace.basisFun (κ i) ℝ).repr x).ofLp i_1 • (EuclideanSpace.basisFun (κ i) ℝ) i_1,
        (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫,
      fun ω ↦ ⟪y, (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫; P] =
    0

Tactic:
← (EuclideanSpace.basisFun _ _).sum_repr y

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝² : IsProbabilityMeasure P
this✝¹ : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
this✝ : (i : ι) → Fintype (κ i) := fun i ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 (κ i → ℝ)
y : WithLp 2 (κ j → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ i_1, ((EuclideanSpace.basisFun (κ i) ℝ).repr x).ofLp i_1 • (EuclideanSpace.basisFun (κ i) ℝ) i_1,
        (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫,
      fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun (κ j) ℝ).repr y).ofLp i • (EuclideanSpace.basisFun (κ j) ℝ) i,
        (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫;
      P] =
    0
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
⊢ IsGaussian (Measure.map (fun ω ↦ (X ω, Y ω)) P)

Tactic:
by
    have := hX.isProbabilityMeasure
    rw [isGaussian_iff_gaussian_charFunDual]
    refine ⟨(∫ x, x ∂P.map X, ∫ y, y ∂P.map Y),
      .diagonalStrongDualProd (covarianceBilinDual (P.map X)) (covarianceBilinDual (P.map Y)),
      isPosSemidef_diagonalStrongDualProd isPosSemidef_covarianceBilinDual
        isPosSemidef_covarianceBilinDual, fun L ↦ ?_⟩
    rw [(indepFun_iff_charFunDual_prod (by fun_prop) (by fun_prop)).1 hXY]
    have : (∫ x, x ∂Measure.map X P, ∫ y, y ∂Measure.map Y P) =
        ContinuousLinearMap.inl ℝ E F (∫ x, x ∂Measure.map X P) +
        ContinuousLinearMap.inr ℝ E F (∫ y, y ∂Measure.map Y P) := by simp
    simp only [this, map_add, ofReal_add, add_mul, diagonalStrongDualProd_apply, add_div,
      add_sub_add_comm, exp_add]
    congr
    · rw [hX.isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
        covarianceBilinDual_self_eq_variance]
      · simp
      · exact hX.isGaussian_map.memLp_two_id
      · exact hX.isGaussian_map.integrable_id
    · rw [hY.isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
        covarianceBilinDual_self_eq_variance]
      · simp
      · exact hY.isGaussian_map.memLp_two_id
      · exact hY.isGaussian_map.integrable_id

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
⊢ ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a = (κ a) (u ×ˢ s)

Tactic:
simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
⊢ (κ a) (u ×ˢ s) / (ν a) u * (ν a) u = (κ a) (u ×ˢ s)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun ι ℝ).repr x).ofLp i • (EuclideanSpace.basisFun ι ℝ) i,
        (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫,
      fun ω ↦ ⟪y, (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫; P] =
    0

Tactic:
← (EuclideanSpace.basisFun _ _).sum_repr y

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun ι ℝ).repr x).ofLp i • (EuclideanSpace.basisFun ι ℝ) i,
        (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫,
      fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun κ ℝ).repr y).ofLp i • (EuclideanSpace.basisFun κ ℝ) i,
        (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫;
      P] =
    0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ (ν a)[fun x ↦ κ.densityProcess ν j a x s | ↑(countableFiltration γ) i] =ᵐ[ν a] fun x ↦ κ.densityProcess ν i a x s

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq ?_ ?_ ?_ ?_ ?_).symm

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun x ↦ κ.densityProcess ν j a x s) (ν a)

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (s_1 : Set γ), MeasurableSet s_1 → (ν a) s_1 < ∞ → IntegrableOn (fun x ↦ κ.densityProcess ν i a x s) s_1 (ν a)

case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (s_1 : Set γ),
    MeasurableSet s_1 →
      (ν a) s_1 < ∞ →
        ∫ (x : γ) in s_1, κ.densityProcess ν i a x s ∂ν a = ∫ (x : γ) in s_1, κ.densityProcess ν j a x s ∂ν a

case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ AEStronglyMeasurable (fun x ↦ κ.densityProcess ν i a x s) (ν a)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x ↦ ∫ (y : Ω), f (x, y) ∂(condDistrib Y X μ) x

Tactic:
by
  rw [condDistrib]; exact hf.integral_kernel_prod_right'

Goal state after:
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable X (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable Y (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa

Goal state after: