awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 μ
have neg : ∀ (h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) 0 μ), MemLp (ε := E) (fun (x : E) ↦ c) 0 μ
Tactic: rcases eq_or_ne p 0 with rfl | hp0
Cleared hypotheses: p, h_Lp
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 μ
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ
have neg₁ : ∀ (hp0 : p ≠ 0), MemLp (ε := E) (fun (x : E) ↦ c) p μ
Tactic: rcases eq_or_ne p 0 with rfl | hp0
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ
have neg : ∀ (h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) ∞ μ) (hp0 : Ne (α := ℝ≥0∞) ∞ 0), MemLp (ε := E) (fun (x : E) ↦ c) ∞ μ
Tactic: rcases eq_or_ne p ∞ with rfl | hptop
Cleared hypotheses: p, h_Lp, hp0
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) ∞ μ
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ
have neg₁ : ∀ (hptop : p ≠ ∞), MemLp (ε := E) (fun (x : E) ↦ c) p μ
Tactic: rcases eq_or_ne p ∞ with rfl | hptop
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ≠ ∞
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ
have neg : Integrable (ε := ℝ) (fun (x : E) ↦ ‖c‖ ^ p.toReal) μ
Tactic: apply (integrable_norm_rpow_iff (by fun_prop) hp0 hptop).1
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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‖) μ
have hf : Integrable (ε := E) (fun (a : E) ↦ a) μ
Tactic: apply Integrable.norm
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 (ε := E) (fun (a : E) ↦ a) μ
have hf : ∀ (hx : ¬Integrable (ε := E) (fun (a : E) ↦ a) μ), c = 0
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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) ↦ ‖c‖ ^ p.toReal) μ
have I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
Tactic: have I : Integrable (fun (x : E) ↦ ‖x‖) μ := by
    apply Integrable.norm
    contrapose hx
    exact integral_undef hx
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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) ↦ ‖c‖ ^ p.toReal) μ
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖c‖ ^ p.toReal) μ
have 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
Tactic: apply (((I.const_mul (2 * ‖c‖ ^ (p.toReal - 1))).add this)).mono' (by fun_prop)
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) μ
⊢ ∀ᵐ (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
have 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
Tactic: filter_upwards [] with y
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ ‖‖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
have 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
Tactic: lift p to ℝ≥0 using hptop
Cleared hypotheses: p, h_Lp, hp0, hptop, this
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) μ
⊢ ‖‖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
have neg : |‖c‖ ^ (↑p : ℝ)| ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
Tactic: simp only [ENNReal.coe_toReal, Real.norm_eq_abs, Pi.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) μ
⊢ |‖c‖ ^ (↑p : ℝ)| ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have neg : ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
Tactic: rw [abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) μ
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have neg : ‖y‖ ≤ ‖c‖ / 2 → ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
Tactic: rcases le_total ‖y‖ (‖c‖ / 2)
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 : ℝ)
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have neg₁ : ‖c‖ / 2 ≤ ‖y‖ → ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
Tactic: rcases le_total ‖y‖ (‖c‖ / 2)
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have this₁ : ‖c‖ ≤ ‖y‖ + ‖y - c‖
Tactic: have : ‖c‖ ≤ ‖y‖ + ‖y - c‖ := Eq.trans_le (by abel_nf) (norm_sub_le y (y - c))
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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‖
⊢ ‖c‖ ^ (↑p : ℝ) ≤ (2 * ‖y - c‖) ^ (↑p : ℝ)
have h₁ : ‖c‖ ≤ 2 * ‖y - c‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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‖
⊢ ‖c‖ ≤ 2 * ‖y - c‖
have linarith : 2 * ‖y - c‖ < ‖c‖ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ ‖c‖ ≤ 2 * ‖y - c‖
have linarith₁ : 2 * ‖y - c‖ < ‖c‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ ‖c‖ ≤ 2 * ‖y - c‖
have linarith₂ : 2 * ‖y - c‖ < ‖c‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ ‖c‖ ≤ 2 * ‖y - c‖
have linarith₃ : 2 * ‖y - c‖ < ‖c‖ → 2 * ‖y‖ - 1 * ‖c‖ + 2 * (‖c‖ - (‖y‖ + ‖y - c‖)) + (2 * ‖y - c‖ - ‖c‖) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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‖
⊢ (2 * ‖y - c‖) ^ (↑p : ℝ) = 0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have rw : HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ) = 0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
Tactic: rw [Real.mul_rpow (by simp) (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ) ≤
    2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have bc : 0 ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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‖
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have calc : ‖c‖ ^ (↑p : ℝ) ≤ (2 * ‖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
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 : ℝ)
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have calc₁ : (2 * ‖y - c‖) ^ (↑p : ℝ) = 0 + 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
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 : ℝ)
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have calc₂ : 0 + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - 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
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 + 1) = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
have rw : ‖c‖ ^ ((↑p : ℝ) - 1) * HPow.hPow (β := ℝ) ‖c‖ 1 = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
Tactic: rw [Real.rpow_add (by positivity), Real.rpow_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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‖
⊢ ‖c‖ ^ ((↑p : ℝ) - 1 + 1) = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
have rw₁ : ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖ = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
Tactic: rw [Real.rpow_add (by positivity), Real.rpow_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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) * ‖c‖ ≤ ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖)
have hbc : ‖c‖ ≤ 2 * ‖y‖
Tactic: gcongr