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
x y : E
rw :
  Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
      ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
have rw₁ : Eq (α := ℝ)
  ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
            ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
          StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
    ℝ)
  ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
Tactic: rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_comm,
    covarianceBilin_eq_covarianceBilinDual]
-- 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
x y : E
rw :
  Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
      ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
      ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
have rw₂ : Eq (α := ℝ)
  ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
            ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
          StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
    ℝ)
  ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
            ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
          StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
    ℝ)
Tactic: rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_comm,
    covarianceBilin_eq_covarianceBilinDual]
-- 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 : IsFiniteMeasure μ
h : MemLp id 2 μ
x : E
⊢ (((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x = Var[fun (u : E) ↦ ⟪x, u⟫; μ]
have rw : Var[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ); μ] = Var[fun (u : E) ↦ ⟪x, u⟫; μ]
Tactic: rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_self_eq_variance 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 : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ (((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y =
    cov[fun (u : E) ↦ ⟪x, u⟫, fun (u : E) ↦ ⟪y, u⟫; μ]
have rw : cov[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ),
    (⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) : (a : E) → ℝ); μ] =
  cov[fun (u : E) ↦ ⟪x, u⟫, fun (u : E) ↦ ⟪y, u⟫; μ]
Tactic: rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_eq_covariance h]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]
have pos : ∀ (h : MemLp id 2 μ), (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]
Tactic: by_cases h : MemLp id 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
pos :
  ∀ (h : MemLp id 2 μ), (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]
have neg : ∀ (h : ¬MemLp id 2 μ), (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]
Tactic: by_cases h : MemLp id 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]
have pos : cov[fun (u : ℝ) ↦ x * u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
Tactic: simp only [covarianceBilin_apply_eq_cov h, RCLike.inner_apply, conj_trivial, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ cov[fun (u : ℝ) ↦ x * u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
have pos : x * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, ← mul_assoc,
      covariance_self aemeasurable_id', Function.id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
pos : x * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
⊢ cov[fun (u : ℝ) ↦ x * u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
have pos₁ : x * (y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ]) = x * y * Var[id; μ]
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, ← mul_assoc,
      covariance_self aemeasurable_id', Function.id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
pos : x * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
pos₁ : x * (y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ]) = x * y * Var[id; μ]
⊢ cov[fun (u : ℝ) ↦ x * u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
have pos₂ : x * y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ] = x * y * Var[id; μ]
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, ← mul_assoc,
      covariance_self aemeasurable_id', Function.id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
pos : x * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
pos₁ : x * (y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ]) = x * y * Var[id; μ]
pos₂ : x * y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ] = x * y * Var[id; μ]
⊢ cov[fun (u : ℝ) ↦ x * u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
have pos₃ : x * y * Var[fun (x : ℝ) ↦ x; μ] = x * y * Var[id; μ]
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, ← mul_assoc,
      covariance_self aemeasurable_id', Function.id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
pos : x * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
pos₁ : x * (y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ]) = x * y * Var[id; μ]
pos₂ : x * y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ] = x * y * Var[id; μ]
pos₃ : x * y * Var[fun (x : ℝ) ↦ x; μ] = x * y * Var[id; μ]
⊢ cov[fun (u : ℝ) ↦ x * u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
have pos₄ : x * y * Var[fun (x : ℝ) ↦ x; μ] = x * y * Var[fun (x : ℝ) ↦ x; μ]
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, ← mul_assoc,
      covariance_self aemeasurable_id', Function.id_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x : ℝ
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) x = HPow.hPow (β := ℕ) x 2 * Var[id; μ]
have rw : x * x * Var[id; μ] = HPow.hPow (β := ℕ) x 2 * Var[id; μ]
Tactic: rw [covarianceBilin_real, pow_two]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x : ℝ
rw : x * x * Var[id; μ] = HPow.hPow (β := ℕ) x 2 * Var[id; μ]
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) x = HPow.hPow (β := ℕ) x 2 * Var[id; μ]
have rw₁ : x * x * Var[id; μ] = x * x * Var[id; μ]
Tactic: rw [covarianceBilin_real, pow_two]
-- 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
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
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (⇑L : (a : E) → F) μ) : (a : F) → F →L[ℝ] ℝ) u : F →L[ℝ] ℝ) : (a : F) → ℝ) v : ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ)
              ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u : E) :
            E →L[ℝ] ℝ) :
          (a : E) → ℝ)
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v : E) :
      ℝ)
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (z : F) ↦
    ⟪u, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫ *
      ⟪v, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫)
  (∫ (z : E),
    ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
        z - ∫ (x : E), id x ∂μ⟫ *
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
        z - ∫ (x : E), id x ∂μ⟫ ∂μ)
Tactic: rw [covarianceBilin_apply, covarianceBilin_apply 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
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
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (z : F) ↦
      ⟪u, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫ *
        ⟪v, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), id x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), id x ∂μ⟫ ∂μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (⇑L : (a : E) → F) μ) : (a : F) → F →L[ℝ] ℝ) u : F →L[ℝ] ℝ) : (a : F) → ℝ) v : ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ)
              ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u : E) :
            E →L[ℝ] ℝ) :
          (a : E) → ℝ)
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v : E) :
      ℝ)
have h₁ : MemLp.{u_2, u_2} (α := F) (m0 := inst_6) id 2 (Measure.map (⇑L : (a : E) → F) μ)
Tactic: rw [covarianceBilin_apply, covarianceBilin_apply 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
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
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (z : F) ↦
      ⟪u, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫ *
        ⟪v, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), id x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), id x ∂μ⟫ ∂μ)
have simp_rw : Eq (α := ℝ)
  (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) 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)⟫)
  (∫ (z : E),
    ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
        z - ∫ (x : E), x ∂μ⟫ *
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
        z - ∫ (x : E), x ∂μ⟫ ∂μ)
Tactic: simp_rw [id, L.integral_id_map (h.integrable (by simp))]
-- 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
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
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) 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)⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
have rw : Eq (α := ℝ)
  (∫ (x : E),
    ⟪u, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
      ⟪v, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ ∂μ)
  (∫ (z : E),
    ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
        z - ∫ (x : E), x ∂μ⟫ *
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
        z - ∫ (x : E), x ∂μ⟫ ∂μ)
Tactic: rw [integral_map]
-- 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
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
rw :
  Eq (α := ℝ)
    (∫ (x : E),
      ⟪u, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ ∂μ)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) 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)⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
have hφ : AEMeasurable.{u_1, u_2} (β := F) (⇑L : (a : E) → F) μ
Tactic: rw [integral_map]
-- 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
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
rw :
  Eq (α := ℝ)
    (∫ (x : E),
      ⟪u, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ ∂μ)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
hφ : AEMeasurable.{u_1, u_2} (β := F) (⇑L : (a : E) → F) μ
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) 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)⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
have hfm : 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: rw [integral_map]
-- 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
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
⊢ Eq (α := ℝ)
    (∫ (x : E),
      ⟪u, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ ∂μ)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
have simp_rw : Eq (α := ℝ) (∫ (x : E), ⟪u, (L : (a : E) → F) (x - ∫ (x : E), x ∂μ)⟫ * ⟪v, (L : (a : E) → F) (x - ∫ (x : E), x ∂μ)⟫ ∂μ)
  (∫ (z : E),
    ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
        z - ∫ (x : E), x ∂μ⟫ *
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
        z - ∫ (x : E), x ∂μ⟫ ∂μ)
Tactic: simp_rw [← map_sub, ← L.adjoint_inner_left]
-- 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
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)
have pos : ∀ (h : MemLp id 2 μ),
  Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)
Tactic: by_cases h : MemLp id 2 μ
-- 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
pos :
  ∀ (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 μ)
have neg : ∀ (h : ¬MemLp id 2 μ),
  Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin (Measure.map (fun (x : E) ↦ c + x) μ)) (covarianceBilin μ)
Tactic: by_cases h : MemLp id 2 μ
-- 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 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 : ℝ)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (hypothesis)
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
⊢ 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 h_Lp : 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