Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun ω ↦ ⟪∑ i, ⟪(basisFun ι ℝ) i, x⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫, fun ω ↦
      ⟪∑ i, ⟪(basisFun ι ℝ) i, y⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫; μ] =
    ∑ i, ∑ j, x.ofLp i * y.ofLp j * cov[X i, X j; μ]

pp: case hX
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪x, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

pp: case hY
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪y, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

pp: case hZ
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

pp: case h
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp id 2 (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

Tactic:
· simp_rw [sum_inner, real_inner_smul_left, basisFun_inner]
    rw [covariance_fun_sum_fun_sum]
    · refine Finset.sum_congr rfl fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_
      rw [covariance_const_mul_left, covariance_const_mul_right]
      ring
    all_goals exact fun i ↦ (hX i).const_mul _

Goal state after:
case hX
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪x, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

case hY
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪y, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

case hZ
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

case h
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp id 2 (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)