Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ∫ (x : E), ⟪u, L x - L (∫ (x : E), x ∂μ)⟫ * ⟪v, L x - L (∫ (x : E), x ∂μ)⟫ ∂μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), x ∂μ⟫ ∂μ

pp: case hφ
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEMeasurable (⇑L) μ

pp: case hfm
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEStronglyMeasurable (fun z ↦ ⟪u, z - L (∫ (x : E), x ∂μ)⟫ * ⟪v, z - L (∫ (x : E), x ∂μ)⟫) (Measure.map (⇑L) μ)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ∫ (x : E), ⟪u, L x - L (∫ (x : E), x ∂μ)⟫ * ⟪v, L x - L (∫ (x : E), x ∂μ)⟫ ∂μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), x ∂μ⟫ ∂μ

case hφ
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEMeasurable (⇑L) μ

case hfm
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEStronglyMeasurable (fun z ↦ ⟪u, z - L (∫ (x : E), x ∂μ)⟫ * ⟪v, z - L (∫ (x : E), x ∂μ)⟫) (Measure.map (⇑L) μ)