awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this_2 : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖y‖ ≤ ‖c‖ / 2
this : ‖c‖ ≤ ‖y‖ + ‖y - c‖
rw : HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ) = 0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
⊢ (2 * ‖y - c‖) ^ (↑p : ℝ) = 0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)

Tactic:
rw [Real.mul_rpow (by simp) (by positivity)]

Premises used: Real.mul_rpow
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this_2 : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖y‖ ≤ ‖c‖ / 2
this : ‖c‖ ≤ ‖y‖ + ‖y - c‖
⊢ HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ) = 0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)

Tactic:
ring
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this_2 : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖y‖ ≤ ‖c‖ / 2
this : ‖c‖ ≤ ‖y‖ + ‖y - c‖
bc : 0 ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖
⊢ 0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ) ≤
    2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this_2 : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖y‖ ≤ ‖c‖ / 2
this : ‖c‖ ≤ ‖y‖ + ‖y - c‖
⊢ 0 ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this_2 : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖y‖ ≤ ‖c‖ / 2
this : ‖c‖ ≤ ‖y‖ + ‖y - c‖
calc : ‖c‖ ^ (↑p : ℝ) ≤ (2 * ‖y - c‖) ^ (↑p : ℝ)
calc₁ : (2 * ‖y - c‖) ^ (↑p : ℝ) = 0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
calc₂ :
  0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ) ≤
    2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)

Tactic:
calc ‖c‖ ^ (p : ℝ)
    _ ≤ (2 * ‖y - c‖) ^ (p : ℝ) := by
      gcongr
      linarith
    _ = 0 + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by
      rw [Real.mul_rpow (by simp) (by positivity)]
      ring
    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by
      gcongr
      positivity

Premises used: Norm.norm, HMul.hMul, HSub.hSub, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ (↑p : ℝ) = ‖c‖ ^ ((↑p : ℝ) - 1 + 1)

Tactic:
abel_nf
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
⊢ 0 < ‖c‖

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
rw : ‖c‖ ^ ((↑p : ℝ) - 1) * HPow.hPow (β := ℝ) ‖c‖ 1 = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
rw₁ rw₂ : ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖ = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
⊢ ‖c‖ ^ ((↑p : ℝ) - 1 + 1) = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖

Tactic:
rw [Real.rpow_add (by positivity), Real.rpow_one]

Premises used: Real.rpow_one, Real.rpow_add
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
hbc : ‖c‖ ≤ 2 * ‖y‖
⊢ ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖ ≤ ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
linarith : 2 * ‖y‖ < ‖c‖ → 2 / 2 = 1
linarith₁ : 2 * ‖y‖ < ‖c‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * ‖y‖ < ‖c‖ → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * ‖y‖ < ‖c‖ → 1 * ‖c‖ - 2 * ‖y‖ + (2 * ‖y‖ - ‖c‖) = 0
⊢ ‖c‖ ≤ 2 * ‖y‖

Tactic:
linarith
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖) = 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + 0

Tactic:
ring
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
bc : 0 ≤ HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
⊢ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + 0 ≤
    2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
⊢ 0 ≤ HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
calc : ‖c‖ ^ (↑p : ℝ) = ‖c‖ ^ ((↑p : ℝ) - 1 + 1)
calc₁ : ‖c‖ ^ ((↑p : ℝ) - 1 + 1) = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
calc₂ : ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖ ≤ ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖)
calc₃ : ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖) = 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + 0
calc₄ :
  2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + 0 ≤
    2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)

Tactic:
calc ‖c‖ ^ (p : ℝ)
    _ = ‖c‖ ^ ((p - 1) + 1 : ℝ) := by abel_nf
    _ = ‖c‖ ^ (p - 1 : ℝ) * ‖c‖ := by rw [Real.rpow_add (by positivity), Real.rpow_one]
    _ ≤ ‖c‖ ^ (p - 1 : ℝ) * (2 * ‖y‖) := by gcongr; linarith
    _ = 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 0 := by ring
    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by gcongr; positivity

Premises used: Norm.norm, HMul.hMul, HSub.hSub, HAdd.hAdd, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
h₁ : ¬MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (0 : ℝ)

Tactic:
rw [covarianceBilinDual, uncenteredCovarianceBilinDual_of_not_memLp]

Premises used: ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, ProbabilityTheory.covarianceBilinDual
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
h₁ : ¬MemLp (ε := E) (id ∘ fun (x : E) ↦ x - ∫ (x : E), x ∂μ) 2 μ
⊢ ¬MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)

Tactic:
rw [(measurableEmbedding_subRight _).memLp_map_measure_iff]

Premises used: MeasurableEmbedding.memLp_map_measure_iff, measurableEmbedding_subRight
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ¬MemLp (ε := E) (id ∘ fun (x : E) ↦ x - ∫ (x : E), x ∂μ) 2 μ

Tactic:
h
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ¬MemLp (ε := E) (id ∘ fun (x : E) ↦ x - ∫ (x : E), x ∂μ) 2 μ

Tactic:
exact h
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
h₁ : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (0 : ℝ)

Tactic:
apply covarianceBilinDual_of_not_memLp'

Premises used: ProbabilityTheory.covarianceBilinDual_of_not_memLp'
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
h₁ : ∀ (h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ), MemLp id 2 μ
⊢ ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ

Tactic:
contrapose h
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ MemLp id 2 μ

Tactic:
memLp_id_of_self_sub_integral h

Premises used: MeasureTheory.memLp_id_of_self_sub_integral
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ MemLp id 2 μ

Tactic:
exact memLp_id_of_self_sub_integral h

Premises used: MeasureTheory.memLp_id_of_self_sub_integral
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
rw :
  Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ)
    (uncenteredCovarianceBilinDual (mE := mE)
      (Measure.map (fun (x : E) ↦ x - @integral _ _ _ _ mE 0 fun (x : E) ↦ x) 0))
    0
rw₁ : Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (uncenteredCovarianceBilinDual (mE := mE) 0) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) 0 0
⊢ Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (covarianceBilinDual (mE := mE) 0) 0

Tactic:
rw [covarianceBilinDual, Measure.map_zero, uncenteredCovarianceBilinDual_zero]

Premises used: ProbabilityTheory.covarianceBilinDual, MeasureTheory.Measure.map_zero, ProbabilityTheory.uncenteredCovarianceBilinDual_zero
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
pos :
  ∀ (h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ),
    Eq (α := ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₁ :
        ℝ)
neg :
  ∀ (h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ),
    Eq (α := ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₁ :
        ℝ)
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)

Tactic:
by_cases h : MemLp (fun x ↦ x - ∫ y, y ∂μ) 2 μ

Premises used: HSub.hSub, MeasureTheory.MemLp, MeasureTheory.integral, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)

Tactic:
have h' : MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ) :=
      (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
h' : MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
pos :
  Eq (α := ℝ)
    ((((uncenteredCovarianceBilinDual (mE := mE) (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) :
                (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              L₁ :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((uncenteredCovarianceBilinDual (mE := mE) (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) :
                (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              L₂ :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
pos₁ :
  Eq (α := ℝ)
    (@integral _ _ _ _ mE (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) fun (x : E) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ))
    (@integral _ _ _ _ mE (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) fun (x : E) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ((L₁ : (a : E) → ℝ) x : ℝ))
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)

Tactic:
simp_rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply h', mul_comm (L₁ _)]

Premises used: ProbabilityTheory.covarianceBilinDual, mul_comm, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, DFunLike.coe
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)

Tactic:
simp [h, covarianceBilinDual_of_not_memLp']

Premises used: ProbabilityTheory.covarianceBilinDual_of_not_memLp'
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L : StrongDual ℝ E
pos :
  ∀ (h : MemLp id 2 μ),
    LE.le (α := ℝ) (0 : ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L :
        ℝ)
neg :
  ∀ (h : ¬MemLp id 2 μ),
    LE.le (α := ℝ) (0 : ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L :
        ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L :
      ℝ)

Tactic:
by_cases h : MemLp id 2 μ

Premises used: id, MeasureTheory.MemLp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L : StrongDual ℝ E
h : MemLp id 2 μ
⊢ 0 ≤
    inner ℝ (E := ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))
      ((StrongDual.toLp (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) 2 :
            (a : StrongDual ℝ E) → ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))
          L :
        ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))
      ((StrongDual.toLp (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) 2 :
            (a : StrongDual ℝ E) → ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))
          L :
        ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))

Tactic:
real_inner_self_nonneg

Premises used: real_inner_self_nonneg
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L : StrongDual ℝ E
h : MemLp id 2 μ
⊢ 0 ≤
    inner ℝ (E := ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))
      ((StrongDual.toLp (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) 2 :
            (a : StrongDual ℝ E) → ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))
          L :
        ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))
      ((StrongDual.toLp (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) 2 :
            (a : StrongDual ℝ E) → ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))
          L :
        ↥(Lp ℝ 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)))

Tactic:
exact real_inner_self_nonneg

Premises used: real_inner_self_nonneg
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L : StrongDual ℝ E
h : ¬MemLp id 2 μ
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L :
      ℝ)

Tactic:
simp [h]
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ AEMeasurable (β := E) (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ

Tactic:
fun_prop