awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := inst_6)
    (fun (z : F) ↦
      ⟪u, HSub.hSub (β := F) z ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (β := F) z ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫)
    (Measure.map (⇑L : (a : E) → F) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEStronglyMeasurable.{u_2, u_2} (α := F) (m₀ := inst_6) id (Measure.map (⇑L : (a : E) → F) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ MemLp.{u_2, u_2} (α := F) (m0 := inst_6) id 2 (Measure.map (⇑L : (a : E) → F) μ)

Tactic:
exact memLp_map_measure_iff (by fun_prop) (by fun_prop) |>.2 (L.comp_memLp' h)

Premises used: Iff.mpr, ContinuousLinearMap.comp_memLp', MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
pos :
  ∀ (h : MemLp id 2 μ),
    Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)
neg :
  ∀ (h : ¬MemLp id 2 μ),
    Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)

Tactic:
by_cases h : MemLp id 2 μ

Premises used: id, MeasureTheory.MemLp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
pos :
  ∀ (x y : E),
    Eq (α := ℝ)
      ((((covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ) : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y :
        ℝ)
      ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)

Tactic:
ext x y
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
⊢ MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)

Tactic:
have h_Lp : MemLp id 2 (μ.map (fun x ↦ c + x)) :=
      (measurableEmbedding_addLeft _).memLp_map_measure_iff.mpr <| (memLp_const c).add h
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
⊢ AEMeasurable (β := E) (fun (x : E) ↦ c + x) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := inst_2)
    (fun (z : E) ↦
      ⟪x, z - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ *
        ⟪y, z - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫)
    (Measure.map (fun (x : E) ↦ c + x) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
pos :
  Eq (α := ℝ)
    (∫ (x_1 : E),
      ⟪x, c + x_1 - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ *
        ⟪y, c + x_1 - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ ∂μ)
    (∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ) : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y :
      ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)

Tactic:
rw [covarianceBilin_apply h_Lp,
      covarianceBilin_apply h, integral_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.covarianceBilin_apply
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
pos :
  ∀ (z : E),
    ⟪x, c + z - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ *
        ⟪y, c + z - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ =
      ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫
⊢ Eq (α := ℝ)
    (∫ (x_1 : E),
      ⟪x, c + x_1 - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ *
        ⟪y, c + x_1 - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ ∂μ)
    (∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ)

Tactic:
congr with z
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
z : E
⊢ AEMeasurable (β := E) (fun (x : E) ↦ c + x) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
z : E
pos :
  ⟪x, c + z - ∫ (x : E), id (c + x) ∂μ⟫ * ⟪y, c + z - ∫ (x : E), id (c + x) ∂μ⟫ =
    ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫
⊢ ⟪x, c + z - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ *
      ⟪y, c + z - @integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ c + x) μ) fun (x : E) ↦ id x⟫ =
    ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫

Tactic:
rw [integral_map (by fun_prop) h_Lp.1]

Premises used: MeasureTheory.integral_map, And.left
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
z : E
pos :
  ⟪x, c + z - ∫ (x : E), c + x ∂μ⟫ * ⟪y, c + z - ∫ (x : E), c + x ∂μ⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫
⊢ ⟪x, c + z - ∫ (x : E), id (c + x) ∂μ⟫ * ⟪y, c + z - ∫ (x : E), id (c + x) ∂μ⟫ =
    ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫

Tactic:
simp only [id_eq]

Premises used: id_eq
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
z : E
pos :
  ⟪x, c + z - HAdd.hAdd (α := E) (∫ (a : E), c ∂μ) (∫ (a : E), a ∂μ)⟫ *
      ⟪y, c + z - HAdd.hAdd (α := E) (∫ (a : E), c ∂μ) (∫ (a : E), a ∂μ)⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫
pos₁ : Integrable (ε := E) (fun (x : E) ↦ x) μ
⊢ ⟪x, c + z - ∫ (x : E), c + x ∂μ⟫ * ⟪y, c + z - ∫ (x : E), c + x ∂μ⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫

Tactic:
rw [integral_add (integrable_const _)]

Premises used: MeasureTheory.integrable_const, MeasureTheory.integral_add
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
z : E
⊢ ⟪x, c + z - HAdd.hAdd (α := E) (∫ (a : E), c ∂μ) (∫ (a : E), a ∂μ)⟫ *
      ⟪y, c + z - HAdd.hAdd (α := E) (∫ (a : E), c ∂μ) (∫ (a : E), a ∂μ)⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
z : E
⊢ LE.le (α := ENNReal) 1 2

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
z : E
⊢ Integrable (ε := E) (fun (x : E) ↦ x) μ

Tactic:
exact h.integrable (by simp)

Premises used: MeasureTheory.MemLp.integrable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
neg :
  ∀ (x x_1 : E),
    Eq (α := ℝ)
      ((((covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ) : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ)
          x_1 :
        ℝ)
      ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)

Tactic:
ext
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x x_1 : E
neg : ¬MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ) : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 :
      ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)

Tactic:
rw [covarianceBilin_of_not_memLp, covarianceBilin_of_not_memLp h]

Premises used: ProbabilityTheory.covarianceBilin_of_not_memLp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x x_1 : E
neg : ¬MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ
⊢ ¬MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)

Tactic:
rw [(measurableEmbedding_addLeft _).memLp_map_measure_iff.not]

Premises used: MeasurableEmbedding.memLp_map_measure_iff, Iff.not, measurableEmbedding_addLeft
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x x_1 : E
neg : ∀ (h : MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ), MemLp id 2 μ
⊢ ¬MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ

Tactic:
contrapose h
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c x x_1 : E
h : MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ
⊢ MemLp (HAdd.hAdd (α := E → E) (fun (x : E) ↦ -c) (id ∘ fun (x : E) ↦ c + x)) 2 μ

Tactic:
(memLp_const (-c)).add h

Premises used: MeasureTheory.MemLp.add, Neg.neg, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c x x_1 : E
h : MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ
h₁ : id = HAdd.hAdd (α := E → E) (fun (x : E) ↦ -c) (id ∘ fun (x : E) ↦ c + x)
⊢ MemLp id 2 μ

Tactic:
convert! (memLp_const (-c)).add h

Premises used: MeasureTheory.MemLp.add, Neg.neg, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c x x_1 : E
h : MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ
h₁ : ∀ (x : E), id x = HAdd.hAdd (α := E → E) (β := E → E) (fun (x : E) ↦ -c) (id ∘ fun (x : E) ↦ c + x) x
⊢ id = HAdd.hAdd (α := E → E) (fun (x : E) ↦ -c) (id ∘ fun (x : E) ↦ c + x)

Tactic:
ext
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsProbabilityMeasure μ
c x x_1 : E
h : MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ
x_2 : E
⊢ id x_2 = HAdd.hAdd (α := E → E) (β := E → E) (fun (x : E) ↦ -c) (id ∘ fun (x : E) ↦ c + x) x_2

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
⊢ ∀ (i : ι), AEMeasurable (X i) μ

Tactic:
have (i : ι) := (hX i).aemeasurable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
rw :
  cov[(fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫) ∘ fun (ω : Ω) ↦
        toLp 2 fun (x : ι) ↦ X x ω,
      (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫) ∘ fun (ω : Ω) ↦
        toLp 2 fun (x : ι) ↦ X x ω;
      μ] =
    cov[X i, X j; μ]
hX₁ :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ))
    (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
hY :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ))
    (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
hZ : AEMeasurable.{u_3, u_2} (β := WithLp 2 (ι → ℝ)) (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ
h :
  MemLp.{u_2, u_2} (α := WithLp 2 (ι → ℝ)) (m0 := measurableSpace 2 (ι → ℝ)) id 2
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
⊢ (((covarianceBilin (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ) :
              (a : WithLp 2 (ι → ℝ)) → WithLp 2 (ι → ℝ) →L[ℝ] ℝ)
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι) :
          WithLp 2 (ι → ℝ) →L[ℝ] ℝ) :
        (a : WithLp 2 (ι → ℝ)) → ℝ)
      ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j : EuclideanSpace ℝ ι) =
    cov[X i, X j; μ]

Tactic:
rw [covarianceBilin_apply_eq_cov, covariance_map]

Premises used: ProbabilityTheory.covarianceBilin_apply_eq_cov, ProbabilityTheory.covariance_map
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
simp :
  cov[(fun (u : WithLp 2 (ι → ℝ)) ↦ u.ofLp i) ∘ fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω,
      (fun (u : WithLp 2 (ι → ℝ)) ↦ u.ofLp j) ∘ fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω; μ] =
    cov[X i, X j; μ]
⊢ cov[(fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫) ∘ fun (ω : Ω) ↦
        toLp 2 fun (x : ι) ↦ X x ω,
      (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫) ∘ fun (ω : Ω) ↦
        toLp 2 fun (x : ι) ↦ X x ω;
      μ] =
    cov[X i, X j; μ]

Tactic:
simp [basisFun_inner]

Premises used: EuclideanSpace.basisFun_inner
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[(fun (u : WithLp 2 (ι → ℝ)) ↦ u.ofLp i) ∘ fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω,
      (fun (u : WithLp 2 (ι → ℝ)) ↦ u.ofLp j) ∘ fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω; μ] =
    cov[X i, X j; μ]

Tactic:
rfl
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
funProp : LE.le.{u_2} (α := MeasurableSpace (WithLp 2 (ι → ℝ))) (measurableSpace 2 (ι → ℝ)) (measurableSpace 2 (ι → ℝ))
funProp₁ :
  MeasurableEmbedding (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ))
    (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
funProp : LE.le.{u_2} (α := MeasurableSpace (WithLp 2 (ι → ℝ))) (measurableSpace 2 (ι → ℝ)) (measurableSpace 2 (ι → ℝ))
funProp₁ :
  MeasurableEmbedding (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ))
    (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫)
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable.{u_3, u_2} (β := WithLp 2 (ι → ℝ)) (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp.{u_2, u_2} (α := WithLp 2 (ι → ℝ)) (m0 := measurableSpace 2 (ι → ℝ)) id 2
    (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)

Tactic:
exact (memLp_map_measure_iff aestronglyMeasurable_id (by fun_prop)).2 (MemLp.of_eval_piLp hX)

Premises used: Iff.mpr, aestronglyMeasurable_id, MeasureTheory.MemLp.of_eval_piLp, MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i : ι
rw : AEMeasurable (X i) μ
⊢ (((covarianceBilin (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ) :
              (a : WithLp 2 (ι → ℝ)) → WithLp 2 (ι → ℝ) →L[ℝ] ℝ)
            ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι) :
          WithLp 2 (ι → ℝ) →L[ℝ] ℝ) :
        (a : WithLp 2 (ι → ℝ)) → ℝ)
      ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι) =
    Var[X i; μ]

Tactic:
rw [covarianceBilin_apply_basisFun hX, covariance_self]

Premises used: ProbabilityTheory.covarianceBilin_apply_basisFun, ProbabilityTheory.covariance_self
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i : ι
⊢ ∀ (i : ι), AEMeasurable (X i) μ

Tactic:
have (i : ι) := (hX i).aemeasurable
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable (X i) μ

Tactic:
fun_prop