awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.CovarianceBilin
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
hμ : MemLp id 2 μ
x : E
⊢ LE.le (α := ℝ) 0 (∫ (z : E), HPow.hPow (β := ℕ) ⟪x, z⟫ 2 ∂μ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ_1 : Measure E
p_1 : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
push_cast :
  MemLp.toLp (HAdd.hAdd (α := (a : E) → 𝕜) (⇑u : (a : E) → 𝕜) (⇑v : (a : E) → 𝕜)) ⋯ =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
⊢ MemLp.toLp (⇑(u + v) : (a : E) → 𝕜) ⋯ =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)

Tactic:
push_cast
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ_1 : Measure E
p_1 : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
rw :
  HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯) =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
hf : MemLp.{u_1, u_2} (ε := 𝕜) (⇑u : (a : E) → 𝕜) p μ
hg : MemLp.{u_1, u_2} (ε := 𝕜) (⇑v : (a : E) → 𝕜) p μ
rw₁ :
  HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯) =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
hf₁ : MemLp.{u_1, u_2} (ε := 𝕜) (⇑u : (a : E) → 𝕜) p μ
hg₁ : MemLp.{u_1, u_2} (ε := 𝕜) (⇑v : (a : E) → 𝕜) p μ
⊢ MemLp.toLp (HAdd.hAdd (α := (a : E) → 𝕜) (⇑u : (a : E) → 𝕜) (⇑v : (a : E) → 𝕜)) ⋯ =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)

Tactic:
rw [MemLp.toLp_add]

Premises used: MeasureTheory.MemLp.toLp_add
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ_1 : Measure E
p_1 : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
push_cast :
  MemLp.toLp (HSMul.hSMul (β := (a : E) → 𝕜) c (⇑L : (a : E) → 𝕜)) ⋯ =
    HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) (id c) (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯)
⊢ MemLp.toLp (⇑(c • L) : (a : E) → 𝕜) ⋯ =
    HSMul.hSMul (α := 𝕜) (β := ↥(Lp 𝕜 p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯)

Tactic:
push_cast
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ_1 : Measure E
p_1 : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
rw :
  HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) c (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯) =
    HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) (id c) (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯)
hf : MemLp.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) p μ
⊢ MemLp.toLp (HSMul.hSMul (β := (a : E) → 𝕜) c (⇑L : (a : E) → 𝕜)) ⋯ =
    HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) (id c) (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯)

Tactic:
rw [MemLp.toLp_const_smul]

Premises used: MeasureTheory.MemLp.toLp_const_smul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
h_Lp : MemLp id p μ
L : StrongDual 𝕜 E
⊢ Eq (α := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ))
    (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯ : ↥(Lp 𝕜 p μ))

Tactic:
simp [toLpₗ, dif_pos h_Lp]

Premises used: dif_pos, StrongDual.toLpₗ
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
h_Lp : ¬MemLp id p μ
L : StrongDual 𝕜 E
⊢ Eq (α := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) (0 : ↥(Lp 𝕜 p μ))

Tactic:
simp [toLpₗ, dif_neg h_Lp]

Premises used: StrongDual.toLpₗ, dif_neg
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
pos :
  ∀ (h_Lp : MemLp id p μ),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
neg :
  ∀ (h_Lp : ¬MemLp id p μ),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
by_cases h_Lp : MemLp id p μ

Premises used: id, MeasureTheory.MemLp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : ¬MemLp id p μ
neg : 0 ≤ ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
simp only [h_Lp, not_false_eq_true, toLpₗ_of_not_memLp, Lp.norm_zero]

Premises used: MeasureTheory.Lp.norm_zero, StrongDual.toLpₗ_of_not_memLp, not_false_eq_true
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : ¬MemLp id p μ
⊢ 0 ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
pos :
  ∀ (hp : p = 0),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
neg :
  ∀ (hp : ¬p = 0),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : p = 0
pos : (eLpNorm.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) p μ).toReal ≤ ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
simp only [h_Lp, toLpₗ_apply, Lp.norm_toLp]

Premises used: MeasureTheory.Lp.norm_toLp, StrongDual.toLpₗ_apply
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : p = 0
⊢ (eLpNorm.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) p μ).toReal ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
simp [hp]
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
pos :
  ∀ (hp_top : p = ∞),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
neg :
  ∀ (hp_top : ¬p = ∞),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : p = ∞
pos :
  ∀ (h_Lp : MemLp id ∞ μ),
    (eLpNormEssSup.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) μ).toReal ≤ ‖L‖ * (eLpNormEssSup id μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
simp only [hp_top, StrongDual.toLpₗ_apply h_Lp, Lp.norm_toLp, eLpNorm_exponent_top] at h_Lp ⊢

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.Lp.norm_toLp, StrongDual.toLpₗ_apply
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
pos :
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
⊢ (eLpNormEssSup.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) μ).toReal ≤ ‖L‖ * (eLpNormEssSup id μ).toReal

Tactic:
simp only [eLpNormEssSup, id_eq]

Premises used: MeasureTheory.eLpNormEssSup, id_eq
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
this :
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
rwa :
  ∀
    (this :
      ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
        (‖L‖ₑ * essSup enorm μ).toReal),
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
rwa₁ :
  ∀
    (this :
      ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
        ‖L‖ₑ.toReal * (essSup enorm μ).toReal),
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (this :
      ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
        ‖L‖ * (essSup enorm μ).toReal),
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)

Tactic:
rwa [ENNReal.essSup_const_mul, ENNReal.toReal_mul, toReal_enorm] at this

Premises used: ENNReal.essSup_const_mul, toReal_enorm, ENNReal.toReal_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
pos :
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)

Tactic:
suffices (essSup (fun x ↦ ‖L x‖ₑ) μ).toReal ≤ (essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ).toReal by
      rwa [ENNReal.essSup_const_mul, ENNReal.toReal_mul, toReal_enorm] at this
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
pos : Ne (α := ℝ≥0∞) (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ) ∞
pos₁ :
  LE.le (α := ℝ≥0∞) (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ)
    (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
pos : ‖L‖ₑ * essSup enorm μ ≠ ∞
⊢ Ne (α := ℝ≥0∞) (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ) ∞

Tactic:
rw [ENNReal.essSup_const_mul]

Premises used: ENNReal.essSup_const_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ ‖L‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ ‖L‖ₑ * essSup enorm μ ≠ ∞

Tactic:
exact ENNReal.mul_ne_top (by simp) h_Lp.eLpNorm_ne_top

Premises used: ENNReal.mul_ne_top, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ LE.le (α := ℝ≥0∞) (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ)
    (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)

Tactic:
essSup_mono_ae <| ae_of_all _ L.le_opNorm_enorm

Premises used: MeasureTheory.ae_of_all, essSup_mono_ae, ContinuousLinearMap.le_opNorm_enorm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ LE.le (α := ℝ≥0∞) (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ)
    (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)

Tactic:
exact essSup_mono_ae <| ae_of_all _ L.le_opNorm_enorm

Premises used: MeasureTheory.ae_of_all, essSup_mono_ae, ContinuousLinearMap.le_opNorm_enorm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
⊢ 0 < p.toReal

Tactic:
simp [ENNReal.toReal_pos_iff, pos_iff_ne_zero, hp, Ne.lt_top hp_top]

Premises used: ENNReal.toReal_pos_iff, Ne.lt_top, pos_iff_ne_zero
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
⊢ 0 < p.toReal

Tactic:
have h0 : 0 < p.toReal := by simp [ENNReal.toReal_pos_iff, pos_iff_ne_zero, hp, Ne.lt_top hp_top]
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
this.trans_eq ?_

Premises used: LE.le.trans_eq
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
refine : (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
refine this.trans_eq ?_

Premises used: LE.le.trans_eq
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
simp : ((‖L‖ₑ ^ p.toReal).toReal * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal) ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
⊢ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
simp only [ENNReal.toReal_mul]

Premises used: ENNReal.toReal_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ 0 ≤ ‖L‖ₑ.toReal ^ p.toReal

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ 0 ≤ (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ 0 ≤ ‖L‖ₑ.toReal

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
rw : ‖L‖ * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
⊢ ((‖L‖ₑ ^ p.toReal).toReal * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal) ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
rw [← ENNReal.toReal_rpow, Real.mul_rpow (by positivity) (by positivity),
      ← Real.rpow_mul (by positivity), mul_inv_cancel₀ h0.ne', Real.rpow_one, toReal_enorm]

Premises used: mul_inv_cancel₀, Real.mul_rpow, toReal_enorm, Real.rpow_one, LT.lt.ne', ENNReal.toReal_rpow, Real.rpow_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ p ≠ 0

Tactic:
simp [hp]
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
rw :
  ‖L‖ * ((∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹).toReal =
    ‖L‖ * ((∫⁻ (x : E), ‖id x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)).toReal
⊢ ‖L‖ * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top, ENNReal.toReal_rpow]

Premises used: MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, ENNReal.toReal_rpow
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ ‖L‖ * ((∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹).toReal =
    ‖L‖ * ((∫⁻ (x : E), ‖id x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)).toReal

Tactic:
simp