awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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) μ)
⊢ 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 : ℝ)
have 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 ∂μ⟫ ∂μ)
Tactic: rw [covarianceBilin_apply h_Lp,
      covarianceBilin_apply h, integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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) μ)
⊢ 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 ∂μ⟫ ∂μ)
have 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 ∂μ⟫
Tactic: congr with z
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 - @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 ∂μ⟫
have 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 ∂μ⟫
Tactic: rw [integral_map (by fun_prop) h_Lp.1]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 - ∫ (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 ∂μ⟫
have 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 ∂μ⟫
Tactic: simp only [id_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 - ∫ (x : E), c + x ∂μ⟫ * ⟪y, c + z - ∫ (x : E), c + x ∂μ⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫
have 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 ∂μ⟫
Tactic: rw [integral_add (integrable_const _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 ∂μ⟫
⊢ ⟪x, c + z - ∫ (x : E), c + x ∂μ⟫ * ⟪y, c + z - ∫ (x : E), c + x ∂μ⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫
have pos₁ : Integrable (ε := E) (fun (x : E) ↦ x) μ
Tactic: rw [integral_add (integrable_const _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 μ
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)
have 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 : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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
⊢ 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 : ℝ)
have neg : ¬MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
Tactic: rw [covarianceBilin_of_not_memLp, covarianceBilin_of_not_memLp h]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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
⊢ ¬MemLp (α := E) (m0 := inst_2) id 2 (Measure.map (fun (x : E) ↦ c + x) μ)
have neg : ¬MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ
Tactic: rw [(measurableEmbedding_addLeft _).memLp_map_measure_iff.not]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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
⊢ ¬MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ
have neg : ∀ (h : MemLp (ε := E) (id ∘ fun (x : E) ↦ c + x) 2 μ), MemLp id 2 μ
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 id 2 μ
have h₁ : id = HAdd.hAdd (α := E → E) (fun (x : E) ↦ -c) (id ∘ fun (x : E) ↦ c + x)
Tactic: convert! (memLp_const (-c)).add h
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 μ
⊢ id = HAdd.hAdd (α := E → E) (fun (x : E) ↦ -c) (id ∘ fun (x : E) ↦ c + x)
have h₁ : ∀ (x : E), id x = HAdd.hAdd (α := E → E) (β := E → E) (fun (x : E) ↦ -c) (id ∘ fun (x : E) ↦ c + x) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (hypothesis)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
⊢ (((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; μ]
have this : ∀ (i : ι), AEMeasurable (X i) μ
Tactic: have (i : ι) := (hX i).aemeasurable
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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) μ
⊢ (((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; μ]
have 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; μ]
Tactic: rw [covarianceBilin_apply_eq_cov, covariance_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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; μ]
⊢ (((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; μ]
have hX₁ : AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ))
  (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫)
  (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
Tactic: rw [covarianceBilin_apply_eq_cov, covariance_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 ω) μ)
⊢ (((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; μ]
have hY : AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace 2 (ι → ℝ))
  (fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫)
  (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
Tactic: rw [covarianceBilin_apply_eq_cov, covariance_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 ω) μ)
⊢ (((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; μ]
have hZ : AEMeasurable.{u_3, u_2} (β := WithLp 2 (ι → ℝ)) (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ
Tactic: rw [covarianceBilin_apply_eq_cov, covariance_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 ω) μ
⊢ (((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; μ]
have h : MemLp.{u_2, u_2} (α := WithLp 2 (ι → ℝ)) (m0 := measurableSpace 2 (ι → ℝ)) id 2
  (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ)
Tactic: rw [covarianceBilin_apply_eq_cov, covariance_map]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 (ι → ℝ)) ↦ ⟪(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; μ]
have 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; μ]
Tactic: simp [basisFun_inner]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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) μ
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫
have funProp : LE.le.{u_2} (α := MeasurableSpace (WithLp 2 (ι → ℝ))) (measurableSpace 2 (ι → ℝ)) (measurableSpace 2 (ι → ℝ))
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 (ι → ℝ))
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, u⟫
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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) μ
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫
have funProp : LE.le.{u_2} (α := MeasurableSpace (WithLp 2 (ι → ℝ))) (measurableSpace 2 (ι → ℝ)) (measurableSpace 2 (ι → ℝ))
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
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 (ι → ℝ))
⊢ Measurable (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (u : WithLp 2 (ι → ℝ)) ↦ ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) j, u⟫
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
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; μ]
have rw : AEMeasurable (X i) μ
Tactic: rw [covarianceBilin_apply_basisFun hX, covariance_self]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (hypothesis)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i : ι
⊢ AEMeasurable (X i) μ
have this : ∀ (i : ι), AEMeasurable (X i) μ
Tactic: have (i : ι) := (hX i).aemeasurable
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (hypothesis)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ) :
                (a : WithLp 2 (ι → ℝ)) → WithLp 2 (ι → ℝ) →L[ℝ] ℝ)
              x :
            WithLp 2 (ι → ℝ) →L[ℝ] ℝ) :
          (a : WithLp 2 (ι → ℝ)) → ℝ)
        y :
      ℝ)
    (∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ] : ℝ)
have this : ∀ (i : ι), AEMeasurable (X i) μ
Tactic: have (i : ι) := (hX i).aemeasurable
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
ι : Type u_2
Ω : Type u_3
inst : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) μ) :
                (a : WithLp 2 (ι → ℝ)) → WithLp 2 (ι → ℝ) →L[ℝ] ℝ)
              x :
            WithLp 2 (ι → ℝ) →L[ℝ] ℝ) :
          (a : WithLp 2 (ι → ℝ)) → ℝ)
        y :
      ℝ)
    (∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ] : ℝ)
have nth_rw : cov[fun (ω : Ω) ↦
    inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
      (∑ i : ι,
        HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, x⟫
          ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
      (toLp 2 fun (x : ι) ↦ X x ω),
    fun (ω : Ω) ↦
    inner.{0, u_2} ℝ (E := WithLp 2 (ι → ℝ))
      (∑ i : ι,
        HSMul.hSMul (β := EuclideanSpace ℝ ι) ⟪(basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i, y⟫
          ((basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
      (toLp 2 fun (x : ι) ↦ X x ω);
    μ] =
  ∑ i : ι, ∑ j : ι, x.ofLp i * y.ofLp j * cov[X i, X j; μ]
Tactic: nth_rw 1 [covarianceBilin_apply_eq_cov, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
    ← (basisFun ι ℝ).sum_repr' y]