awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T S : E →L[𝕜] E
x : E
⊢ (T + S).rayleighQuotient x = T.rayleighQuotient x + S.rayleighQuotient x

Tactic:
simp [rayleighQuotient, reApplyInnerSelf_apply, inner_add_left, add_div]

Premises used: inner_add_left, ContinuousLinearMap.reApplyInnerSelf_apply, ContinuousLinearMap.rayleighQuotient, add_div
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ rayleighQuotient.{u_1, u_2} (𝕜 := 𝕜) 0 x = 0

Tactic:
simp [reApplyInnerSelf_apply]

Premises used: ContinuousLinearMap.reApplyInnerSelf_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
⊢ T.rayleighQuotient 0 = 0

Tactic:
simp [reApplyInnerSelf_apply]

Premises used: ContinuousLinearMap.reApplyInnerSelf_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ (-T).rayleighQuotient x = -T.rayleighQuotient x

Tactic:
simp [rayleighQuotient, reApplyInnerSelf_apply, neg_div]

Premises used: neg_div, ContinuousLinearMap.reApplyInnerSelf_apply, ContinuousLinearMap.rayleighQuotient
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ T.rayleighQuotient (-x) = T.rayleighQuotient x

Tactic:
simp [rayleighQuotient, reApplyInnerSelf_apply]

Premises used: ContinuousLinearMap.reApplyInnerSelf_apply, ContinuousLinearMap.rayleighQuotient
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
h : ∀ (a : ℝ), a ∈ T.rayleighQuotient '' {0}ᶜ ↔ a ∈ T.rayleighQuotient '' sphere 0 r
⊢ T.rayleighQuotient '' {0}ᶜ = T.rayleighQuotient '' sphere 0 r

Tactic:
ext a
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
h : a ∈ T.rayleighQuotient '' {0}ᶜ → a ∈ T.rayleighQuotient '' sphere 0 r
h₁ : a ∈ T.rayleighQuotient '' sphere 0 r → a ∈ T.rayleighQuotient '' {0}ᶜ
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ ↔ a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
⊢ c ≠ 0

Tactic:
simp [c, hx, hr.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
⊢ c ≠ 0

Tactic:
have : c ≠ 0 := by simp [c, hx, hr.ne']
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
this : c ≠ 0
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
⟨c • x, ?_, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, HSMul.hSMul
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
this : c ≠ 0
h : Membership.mem (γ := Set E) (sphere 0 r) (c • x)
h₁ : T.rayleighQuotient (c • x) = a
⊢ a ∈ T.rayleighQuotient '' sphere 0 r

Tactic:
refine ⟨c • x, ?_, ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
this : c ≠ 0
⊢ Membership.mem (γ := Set E) (sphere 0 r) (c • x)

Tactic:
simp [field, c, norm_smul, abs_of_pos hr]

Premises used: norm_smul, abs_of_pos
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
this : c ≠ 0
h : T.rayleighQuotient x = a
⊢ T.rayleighQuotient (c • x) = a

Tactic:
rw [T.rayleigh_smul x this]

Premises used: ContinuousLinearMap.rayleigh_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
this : c ≠ 0
⊢ T.rayleighQuotient x = a

Tactic:
hxT
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := HMul.hMul (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) (↑r : 𝕜)
this : c ≠ 0
⊢ T.rayleighQuotient x = a

Tactic:
exact hxT
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : Membership.mem (γ := Set E) (sphere 0 r) x
hxT : T.rayleighQuotient x = a
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ

Tactic:
⟨x, ne_zero_of_mem_sphere hr.ne' ⟨x, hx⟩, hxT⟩

Premises used: Set.Mem, setOf, Subtype.mk, ne_zero_of_mem_sphere, LT.lt.ne', And.intro, Exists.intro, Set.image
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : Membership.mem (γ := Set E) (sphere 0 r) x
hxT : T.rayleighQuotient x = a
⊢ a ∈ T.rayleighQuotient '' {0}ᶜ

Tactic:
exact ⟨x, ne_zero_of_mem_sphere hr.ne' ⟨x, hx⟩, hxT⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
⊢ Eq (α := ℝ) (⨆ (x : (↑{0}ᶜ : Type u_2)), T.rayleighQuotient (↑x : E))
    (⨆ (x : (↑(sphere 0 r) : Type u_2)), T.rayleighQuotient (↑x : E))

Tactic:
simp only [← @sSup_image' _ _ _ _ (rayleighQuotient T),
      T.image_rayleigh_eq_image_rayleigh_sphere hr]

Premises used: ContinuousLinearMap.image_rayleigh_eq_image_rayleigh_sphere, sSup_image'
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
⊢ Eq (α := ℝ) (⨅ (x : (↑{0}ᶜ : Type u_2)), T.rayleighQuotient (↑x : E))
    (⨅ (x : (↑(sphere 0 r) : Type u_2)), T.rayleighQuotient (↑x : E))

Tactic:
simp only [← @sInf_image' _ _ _ _ (rayleighQuotient T),
      T.image_rayleigh_eq_image_rayleigh_sphere hr]

Premises used: ContinuousLinearMap.image_rayleigh_eq_image_rayleigh_sphere, sInf_image'
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
grw : ‖T‖ * (HPow.hPow (β := ℕ) ‖x‖ 2 / HPow.hPow (β := ℕ) ‖x‖ 2) ≤ ‖T‖
⊢ |T.rayleighQuotient x| ≤ ‖T‖

Tactic:
grw [rayleighQuotient, reApplyInnerSelf_apply, abs_div, abs_sq, abs_re_le_norm,
    norm_inner_le_norm, le_opNorm, mul_assoc, ← sq, mul_div_assoc]

Premises used: RCLike.abs_re_le_norm, ContinuousLinearMap.le_opNorm, mul_assoc, mul_div_assoc, abs_div, abs_sq, sq, ContinuousLinearMap.reApplyInnerSelf_apply, ContinuousLinearMap.rayleighQuotient, norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ ‖T‖ * (HPow.hPow (β := ℕ) ‖x‖ 2 / HPow.hPow (β := ℕ) ‖x‖ 2) ≤ ‖T‖

Tactic:
mul_le_of_le_one_right T.opNorm_nonneg (div_self_le_one (‖x‖ ^ 2))

Premises used: Norm.norm, mul_le_of_le_one_right, div_self_le_one, HPow.hPow, ContinuousLinearMap.opNorm_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ ‖T‖ * (HPow.hPow (β := ℕ) ‖x‖ 2 / HPow.hPow (β := ℕ) ‖x‖ 2) ≤ ‖T‖

Tactic:
exact mul_le_of_le_one_right T.opNorm_nonneg (div_self_le_one (‖x‖ ^ 2))

Premises used: Norm.norm, mul_le_of_le_one_right, div_self_le_one, HPow.hPow, ContinuousLinearMap.opNorm_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
⊢ BddAbove (α := ℝ) (Set.range fun (x : E) ↦ |T.rayleighQuotient x|)

Tactic:
⟨‖T‖, fun _ ⟨y, h⟩ ↦ h ▸ T.rayleighQuotient_le_norm y⟩

Premises used: Norm.norm, Eq.rec, LE.le, ContinuousLinearMap.rayleighQuotient_le_norm, BddAbove, Set.Nonempty, _private.0.ContinuousLinearMap.bddAbove_rayleighQuotient.match_1, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
set :
  let M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|;
  ‖T‖ = M
⊢ ‖T‖ = ⨆ (x : E), |T.rayleighQuotient x|

Tactic:
set M := ⨆ x, |T.rayleighQuotient x|
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
⊢ 0 ≤ M

Tactic:
have nonneg : 0 ≤ M := le_ciSup_of_le T.bddAbove_rayleighQuotient 0 (abs_nonneg _)
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
⊢ |T.rayleighQuotient x| ≤ M

Tactic:
have hM : |T.rayleighQuotient x| ≤ M := le_ciSup T.bddAbove_rayleighQuotient x
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
pos :
  ∀ (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
neg :
  ∀ (hx : ¬0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
by_cases hx : 0 < ‖x‖ ^ 2
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2
pos :
  ∀ (hM : |T.reApplyInnerSelf x / HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₁ :
  ∀ (hM : |T.reApplyInnerSelf x| / |HPow.hPow (β := ℕ) ‖x‖ 2| ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₂ :
  ∀ (hM : |T.reApplyInnerSelf x| / HPow.hPow (β := ℕ) ‖x‖ 2 ≤ M) (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2),
    |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₃ :
  ∀ (hM : HDiv.hDiv (α := ℝ) (|(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| : ℝ) (HPow.hPow (β := ℕ) ‖x‖ 2) ≤ M)
    (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
pos₄ pos₅ pos₆ pos₇ :
  ∀ (hM : |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2)
    (hx : 0 < HPow.hPow (β := ℕ) ‖x‖ 2), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM

Premises used: div_le_iff₀, abs_div, abs_sq, ContinuousLinearMap.reApplyInnerSelf, ContinuousLinearMap.rayleighQuotient
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.rayleighQuotient x| ≤ M
hx : ¬0 < HPow.hPow (β := ℕ) ‖x‖ 2
⊢ |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
⊢ ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
have hM x : |re ⟪T x, x⟫| ≤ M * ‖x‖ ^ 2 := by
    have hM : |T.rayleighQuotient x| ≤ M := le_ciSup T.bddAbove_rayleighQuotient x
    by_cases hx : 0 < ‖x‖ ^ 2
    · rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
    · simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ‖T‖ = M

Tactic:
le_antisymm ?_ (ciSup_le T.rayleighQuotient_le_norm)

Premises used: ContinuousLinearMap.rayleighQuotient_le_norm, le_antisymm, ciSup_le
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
refine : ‖T‖ ≤ M
⊢ ‖T‖ = M

Tactic:
refine le_antisymm ?_ (ciSup_le T.rayleighQuotient_le_norm)

Premises used: ContinuousLinearMap.rayleighQuotient_le_norm, le_antisymm, ciSup_le
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ‖T‖ ≤ M

Tactic:
opNorm_le_of_re_inner_le nonneg fun x y hx hy ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_of_re_inner_le
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
refine : ∀ (x y : E) (hx : ‖x‖ = 1) (hy : ‖y‖ = 1), (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M
⊢ ‖T‖ ≤ M

Tactic:
refine opNorm_le_of_re_inner_le nonneg fun x y hx hy ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_of_re_inner_le
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
transitivity :
  (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4
transitivity₁ : M * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4 ≤ M
⊢ (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M

Tactic:
transitivity M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4

Premises used: Norm.norm, HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        (HAdd.hAdd (β := 𝕜) ⟪(T : (a : E) → E) x, y⟫_𝕜 ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, y⟫_𝕜 : 𝕜)) :
      ℝ)
    ((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) 2 (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜) : 𝕜)) : ℝ)

Tactic:
have key := congrArg re (add_conj ⟪T x, y⟫)
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
key :
  Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        (HAdd.hAdd (β := 𝕜) ⟪(T : (a : E) → E) x, y⟫_𝕜 ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, y⟫_𝕜 : 𝕜)) :
      ℝ)
    ((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) 2 (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜) : 𝕜)) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 : ℝ)
      ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫_𝕜 : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 : ℝ)

Tactic:
rw [map_add, conj_inner_symm, ← coe_coe, ← hT, coe_coe, re_mul_ofReal, ofNat_re] at key

Premises used: RCLike.ofNat_re, map_add, ContinuousLinearMap.coe_coe, RCLike.re_mul_ofReal, InnerProductSpace.conj_inner_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
key :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 : ℝ)
      ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫_𝕜 : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 : ℝ)
⊢ (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4

Tactic:
grind [inner_add_left, inner_add_right, inner_sub_left, inner_sub_right]

Premises used: inner_add_left, inner_add_right, inner_sub_left, inner_sub_right
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
rw : M * (2 * (HPow.hPow (α := ℝ) (β := ℕ) 1 2 + HPow.hPow (α := ℝ) (β := ℕ) 1 2)) / 4 ≤ M
⊢ M * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4 ≤ M

Tactic:
rw [parallelogram_law_with_norm 𝕜 x y, hx, hy]

Premises used: parallelogram_law_with_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
M : ℝ := ⨆ (x : E), |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |(re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜| ≤ M * HPow.hPow (β := ℕ) ‖x‖ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ M * (2 * (HPow.hPow (α := ℝ) (β := ℕ) 1 2 + HPow.hPow (α := ℝ) (β := ℕ) 1 2)) / 4 ≤ M

Tactic:
grind
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
pos :
  ∀ (hT0 : T = 0),
    ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c
neg :
  ∀ (hT0 : ¬T = 0),
    ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c
⊢ ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c

Tactic:
by_cases hT0 : T = 0
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : T = 0
⊢ HPow.hPow (β := ℕ) t 2 / (2 * t) > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : T = 0
⊢ ∀ (x : E),
    T.rayleighQuotient x ≤
      (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - HPow.hPow (β := ℕ) t 2 / (2 * t)

Tactic:
simp [hT0]
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : T = 0
⊢ ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c

Tactic:
exact ⟨t ^ 2 / (2 * t), by positivity, by simp [hT0]⟩