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
inst_2 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
calc :
  norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) =
    norm (E := ℝ) (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
calc₁ :
  LE.le (α := ℝ) (∫ (x : E), norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
    (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ)
calc₂ : ∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ = ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
⊢ norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ

Tactic:
calc ‖uncenteredCovarianceBilinDual μ L₁ L₂‖
  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilinDual_apply h]
  _ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := (norm_integral_le_integral_norm _).trans (by simp)
  _ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ := by
    refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
    · simp_rw [← norm_mul]
      exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm
    · simp_rw [mul_assoc]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
      refine Integrable.const_mul ?_ _
      exact h.integrable_norm_pow (by simp)
    · simp only
      rw [mul_assoc]
      gcongr
      · exact ContinuousLinearMap.le_opNorm L₁ x
      · exact ContinuousLinearMap.le_opNorm L₂ x
  _ = ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
    rw [← integral_const_mul]
    congr with x
    ring

Premises used: MeasureTheory.norm_integral_le_integral_norm, LE.le.trans, DFunLike.coe, ProbabilityTheory.uncenteredCovarianceBilinDual
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
h : ∀ (x : E), id x = x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
⊢ Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ

Tactic:
ext
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
x : E
⊢ id x = x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
⊢ Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ

Tactic:
have : (id : E → E) = fun x ↦ x - ∫ x, x ∂μ + ∫ x, x ∂μ := by ext; simp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
rw : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ) p μ
⊢ MemLp id p μ

Tactic:
rw [this]
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
apply : MemLp (ε := E) (fun (x : E) ↦ ∫ (x : E), x ∂μ) p μ
⊢ MemLp (ε := E) (fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ) p μ

Tactic:
apply h_Lp.add

Premises used: MeasureTheory.MemLp.add
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
set :
  let c : E := ∫ (x : E), x ∂μ;
  ∀ (h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ)
    (this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c), MemLp (ε := E) (fun (x : E) ↦ c) p μ
⊢ MemLp (ε := E) (fun (x : E) ↦ ∫ (x : E), x ∂μ) p μ

Tactic:
set c := ∫ x, x ∂μ
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
pos : ∀ (hx : c = 0), MemLp (ε := E) (fun (x : E) ↦ c) p μ
neg : ∀ (hx : ¬c = 0), MemLp (ε := E) (fun (x : E) ↦ c) p μ
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ

Tactic:
by_cases hx : c = 0
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : c = 0
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
neg : ∀ (h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) 0 μ), MemLp (ε := E) (fun (x : E) ↦ c) 0 μ
neg₁ : ∀ (hp0 : p ≠ 0), MemLp (ε := E) (fun (x : E) ↦ c) p μ
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ

Tactic:
rcases eq_or_ne p 0 with rfl | hp0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) 0 μ
⊢ MemLp (ε := E) (fun (x : E) ↦ c) 0 μ

Tactic:
simp [aestronglyMeasurable_const]

Premises used: MeasureTheory.aestronglyMeasurable_const
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
neg :
  ∀ (h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) ∞ μ) (hp0 : Ne (α := ℝ≥0∞) ∞ 0), MemLp (ε := E) (fun (x : E) ↦ c) ∞ μ
neg₁ : ∀ (hptop : p ≠ ∞), MemLp (ε := E) (fun (x : E) ↦ c) p μ
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ

Tactic:
rcases eq_or_ne p ∞ with rfl | hptop

Premises used: eq_or_ne, Top.top, rfl
-- 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 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) ∞ μ
hp0 : Ne (α := ℝ≥0∞) ∞ 0
⊢ MemLp (ε := E) (fun (x : E) ↦ c) ∞ μ

Tactic:
memLp_top_const c

Premises used: MeasureTheory.memLp_top_const
-- 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 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) ∞ μ
hp0 : Ne (α := ℝ≥0∞) ∞ 0
⊢ MemLp (ε := E) (fun (x : E) ↦ c) ∞ μ

Tactic:
exact memLp_top_const c

Premises used: MeasureTheory.memLp_top_const
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
⊢ AEStronglyMeasurable (β := E) (fun (x : E) ↦ c) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
neg : Integrable (ε := ℝ) (fun (x : E) ↦ ‖c‖ ^ p.toReal) μ
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ

Tactic:
apply (integrable_norm_rpow_iff (by fun_prop) hp0 hptop).1

Premises used: MeasureTheory.integrable_norm_rpow_iff, Iff.mp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
hf : Integrable (ε := E) (fun (a : E) ↦ a) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ

Tactic:
apply Integrable.norm

Premises used: MeasureTheory.Integrable.norm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
hf : ∀ (hx : ¬Integrable (ε := E) (fun (a : E) ↦ a) μ), c = 0
⊢ Integrable (ε := E) (fun (a : E) ↦ a) μ

Tactic:
contrapose hx
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hp0 : p ≠ 0
hptop : p ≠ ∞
hx : ¬Integrable (ε := E) (fun (a : E) ↦ a) μ
⊢ c = 0

Tactic:
integral_undef hx

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hp0 : p ≠ 0
hptop : p ≠ ∞
hx : ¬Integrable (ε := E) (fun (a : E) ↦ a) μ
⊢ c = 0

Tactic:
exact integral_undef hx

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ

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

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

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

Tactic:
apply (((I.const_mul (2 * ‖c‖ ^ (p.toReal - 1))).add this)).mono' (by fun_prop)

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

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

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

Tactic:
lift p to ℝ≥0 using hptop
-- 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) μ
neg : |‖c‖ ^ (↑p : ℝ)| ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
⊢ ‖‖c‖ ^ (↑p : ℝ≥0∞).toReal‖ ≤
    HAdd.hAdd (α := E → ℝ) (β := E → ℝ) (fun (x : E) ↦ 2 * ‖c‖ ^ ((↑p : ℝ≥0∞).toReal - 1) * ‖x‖)
      (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) y

Tactic:
simp only [ENNReal.coe_toReal, Real.norm_eq_abs, Pi.add_apply]

Premises used: ENNReal.coe_toReal, Pi.add_apply, Real.norm_eq_abs
-- 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) μ
⊢ 0 ≤ ‖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) μ
neg : ‖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:
rw [abs_of_nonneg (by positivity)]

Premises used: abs_of_nonneg
-- 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) μ
neg :
  ‖y‖ ≤ ‖c‖ / 2 → ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
neg₁ :
  ‖c‖ / 2 ≤ ‖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:
rcases le_total ‖y‖ (‖c‖ / 2)

Premises used: Norm.norm, HDiv.hDiv, le_total, OfNat.ofNat
-- 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 : ‖y‖ ≤ ‖c‖ / 2
⊢ ‖c‖ = ‖y - (y - c)‖

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 : ‖y‖ ≤ ‖c‖ / 2
⊢ ‖c‖ ≤ ‖y‖ + ‖y - c‖

Tactic:
have : ‖c‖ ≤ ‖y‖ + ‖y - c‖ := Eq.trans_le (by abel_nf) (norm_sub_le y (y - c))
-- 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‖
h₁ : ‖c‖ ≤ 2 * ‖y - c‖
⊢ ‖c‖ ^ (↑p : ℝ) ≤ (2 * ‖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‖
linarith : 2 * ‖y - c‖ < ‖c‖ → 2 / 2 = 1
linarith₁ : 2 * ‖y - c‖ < ‖c‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * ‖y - c‖ < ‖c‖ → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * ‖y - c‖ < ‖c‖ → 2 * ‖y‖ - 1 * ‖c‖ + 2 * (‖c‖ - (‖y‖ + ‖y - c‖)) + (2 * ‖y - c‖ - ‖c‖) = 0
linarith₄ : 2 * ‖y - c‖ < ‖c‖ → GT.gt (α := ℝ) 2 0
⊢ ‖c‖ ≤ 2 * ‖y - c‖

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_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‖
⊢ LE.le (α := ℝ) 0 2

Tactic:
simp
-- 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 ≤ ‖y - c‖

Tactic:
positivity