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 : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : ¬T = 0
neg :
  ∀ (c : ℝ) (hc0 : c > 0)
    (hc :
      ∀ (x : E),
        c * ‖x‖ ≤
          norm (E := E)
            ((HSub.hSub (α := E →L[𝕜] E)
                    ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E)
                    T :
                  (a : E) → E)
                x :
              E)),
    ∃ 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:
obtain ⟨c, hc0, hc⟩ := antilipschitzWith_iff_exists_mul_le_norm.mp
    (antilipschitz_of_isEmbedding _ (isHomeomorph_of_isUnit hT').isEmbedding)

Premises used: IsHomeomorph.isEmbedding, ContinuousLinearMap.antilipschitz_of_isEmbedding, Iff.mp, ContinuousLinearMap.isHomeomorph_of_isUnit, antilipschitzWith_iff_exists_mul_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
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc :
  ∀ (x : E),
    c * ‖x‖ ≤
      norm (E := E)
        ((HSub.hSub (α := E →L[𝕜] E)
                ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
              (a : E) → E)
            x :
          E)
⊢ min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + 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
c : ℝ
hc0 : c > 0
hc :
  ∀ (x : E),
    c * ‖x‖ ≤
      norm (E := E)
        ((HSub.hSub (α := E →L[𝕜] E)
                ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
              (a : E) → E)
            x :
          E)
neg :
  ∀ (x : E),
    T.rayleighQuotient x ≤
      (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) -
        min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t))
⊢ ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c

Tactic:
refine ⟨min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t)), by positivity, fun 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
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc :
  ∀ (x : E),
    c * ‖x‖ ≤
      norm (E := E)
        ((HSub.hSub (α := E →L[𝕜] E)
                ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
              (a : E) → E)
            x :
          E)
x : E
pos :
  ∀ (hx : x = 0),
    T.rayleighQuotient x ≤
      (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) -
        min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t))
neg :
  ∀ (hx : ¬x = 0),
    T.rayleighQuotient x ≤
      (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) -
        min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t))
⊢ T.rayleighQuotient x ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) -
      min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t))

Tactic:
by_cases hx : x = 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
c : ℝ
hc0 : c > 0
hc :
  ∀ (x : E),
    c * ‖x‖ ≤
      norm (E := E)
        ((HSub.hSub (α := E →L[𝕜] E)
                ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
              (a : E) → E)
            x :
          E)
x : E
hx : x = 0
⊢ T.rayleighQuotient x ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) -
      min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t))

Tactic:
simp [hx]
-- 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 : ℝ
hc0 : c > 0
hc :
  ∀ (x : E),
    c * ‖x‖ ≤
      norm (E := E)
        ((HSub.hSub (α := E →L[𝕜] E)
                ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
              (a : E) → E)
            x :
          E)
x : E
hx : ¬x = 0
this :
  T.rayleighQuotient x ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - HPow.hPow (β := ℕ) c 2 / (2 * t)
grw :
  (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - HPow.hPow (β := ℕ) c 2 / (2 * t) ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) -
      min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t))
grw₁ grw₂ :
  (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - HPow.hPow (β := ℕ) c 2 / (2 * t) ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - HPow.hPow (β := ℕ) c 2 / (2 * t)
⊢ T.rayleighQuotient x ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) -
      min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t))

Tactic:
grw [this, min_le_left]

Premises used: min_le_left
-- 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 : ℝ
hc0 : c > 0
hc :
  ∀ (x : E),
    c * ‖x‖ ≤
      norm (E := E)
        ((HSub.hSub (α := E →L[𝕜] E)
                ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
              (a : E) → E)
            x :
          E)
x : E
hx : ¬x = 0
neg :
  T.rayleighQuotient x ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - HPow.hPow (β := ℕ) c 2 / (2 * t)
⊢ T.rayleighQuotient x ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) -
      min (HPow.hPow (β := ℕ) c 2 / (2 * t)) ((HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t))

Tactic:
suffices T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - c ^ 2 / (2 * t) by
    grw [this, min_le_left]
-- 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 : ℝ
hc0 : c > 0
hc :
  ∀ (x : E),
    c * ‖x‖ ≤
      norm (E := E)
        ((HSub.hSub (α := E →L[𝕜] E)
                ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
              (a : E) → E)
            x :
          E)
x : E
hx : ¬x = 0
⊢ c * ‖x‖ ≤
    norm (E := E)
      ((HSub.hSub (α := E →L[𝕜] E)
              ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
            (a : E) → E)
          x :
        E)

Tactic:
specialize hc 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
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
x : E
hx : ¬x = 0
hc :
  c * ‖x‖ ≤
    norm (E := E)
      ((HSub.hSub (α := E →L[𝕜] E)
              ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
            (a : E) → E)
          x :
        E)
⊢ 0 ≤ c * ‖x‖

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
c : ℝ
hc0 : c > 0
x : E
hx : ¬x = 0
hc :
  c * ‖x‖ ≤
    norm (E := E)
      ((HSub.hSub (α := E →L[𝕜] E)
              ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
            (a : E) → E)
          x :
        E)
⊢ 0 ≤
    norm (E := E)
      ((HSub.hSub (α := E →L[𝕜] E)
              ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
            (a : E) → E)
          x :
        E)

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
c : ℝ
hc0 : c > 0
x : E
hx : ¬x = 0
hc :
  c * ‖x‖ ≤
    norm (E := E)
      ((HSub.hSub (α := E →L[𝕜] E)
              ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t) : E →L[𝕜] E) T :
            (a : E) → E)
          x :
        E)
⊢ HPow.hPow (β := ℕ) (c * ‖x‖) 2 ≤
    HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜) x‖ 2 -
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
          ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜) x⟫_𝕜 :
            ℝ) +
      HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) x : E)) 2

Tactic:
rw [← sq_le_sq₀ (by positivity) (by positivity), sub_apply, algebraMap_apply,
    norm_sub_sq (𝕜 := 𝕜), inner_re_symm] at hc

Premises used: norm_sub_sq, inner_re_symm, ContinuousLinearMap.sub_apply, sq_le_sq₀, ContinuousLinearMap.algebraMap_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 : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
x : E
hx : ¬x = 0
hc :
  HPow.hPow (β := ℕ) (c * ‖x‖) 2 ≤
    HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜) x‖ 2 -
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
          ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜) x⟫_𝕜 :
            ℝ) +
      HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) x : E)) 2
⊢ HPow.hPow (β := ℕ) (c * ‖x‖) 2 ≤
    HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜) x‖ 2 -
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
          ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜) x⟫_𝕜 :
            ℝ) +
      HPow.hPow (β := ℕ) (‖T‖ * ‖x‖) 2

Tactic:
grw [le_opNorm] at hc

Premises used: ContinuousLinearMap.le_opNorm
-- 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 : ℝ
hc0 : c > 0
x : E
hx : ¬x = 0
hc :
  HPow.hPow (β := ℕ) (c * ‖x‖) 2 ≤
    HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜) x‖ 2 -
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
          ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜) x⟫_𝕜 :
            ℝ) +
      HPow.hPow (β := ℕ) (‖T‖ * ‖x‖) 2
⊢ HPow.hPow (β := ℕ) (c * ‖x‖) 2 ≤
    HPow.hPow (β := ℕ) (t * ‖x‖) 2 - 2 * HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜 : ℝ) +
      HPow.hPow (β := ℕ) (‖T‖ * ‖x‖) 2

Tactic:
simp [inner_smul_right, norm_smul, abs_of_pos ht] at hc

Premises used: norm_smul, inner_smul_right, 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
t : ℝ
ht : 0 < t
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) t : 𝕜)
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
x : E
hx : ¬x = 0
hc :
  HPow.hPow (β := ℕ) (c * ‖x‖) 2 ≤
    HPow.hPow (β := ℕ) (t * ‖x‖) 2 - 2 * HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜 : ℝ) +
      HPow.hPow (β := ℕ) (‖T‖ * ‖x‖) 2
neg :
  HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜 : ℝ) t * 2 ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2 - HPow.hPow (β := ℕ) c 2)
⊢ HDiv.hDiv (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜 : ℝ) (HPow.hPow (β := ℕ) ‖x‖ 2) ≤
    (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - HPow.hPow (β := ℕ) c 2 / (2 * t)

Tactic:
field_simp
-- 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 : ℝ
hc0 : c > 0
x : E
hx : ¬x = 0
hc :
  HPow.hPow (β := ℕ) (c * ‖x‖) 2 ≤
    HPow.hPow (β := ℕ) (t * ‖x‖) 2 - 2 * HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜 : ℝ) +
      HPow.hPow (β := ℕ) (‖T‖ * ‖x‖) 2
⊢ HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫_𝕜 : ℝ) t * 2 ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2 - HPow.hPow (β := ℕ) c 2)

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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
pos : ∀ (hT0 : T = 0), ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
neg : ∀ (hT0 : ¬T = 0), ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε

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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT0 : T = 0
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε

Tactic:
simp [hT0, spectrum.mem_resolventSet_iff] at hT'

Premises used: spectrum.mem_resolventSet_iff
-- 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT0 : ¬T = 0
⊢ 0 < ‖T‖

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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT0 : ¬T = 0
neg :
  ∀ (ε : ℝ) (hε0 : ε > 0)
    (hε : ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε),
    ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε

Tactic:
obtain ⟨ε, hε0, hε⟩ := T.rayleighQuotient_le_of_mem_resolventSet ‖T‖ (by positivity) hT'

Premises used: Norm.norm, _private.0.ContinuousLinearMap.rayleighQuotient_le_of_mem_resolventSet
-- 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT0 : ¬T = 0
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε

Tactic:
⟨ε, hε0, fun x ↦ ?_⟩

Premises used: And.intro, 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT0 : ¬T = 0
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε
neg : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε

Tactic:
refine ⟨ε, hε0, fun 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT0 : ¬T = 0
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε
x : E
neg : (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε ≤ ‖T‖ - ε
⊢ T.rayleighQuotient x ≤ ‖T‖ - ε

Tactic:
grw [hε]
-- 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT0 : ¬T = 0
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε
x : E
neg : ‖T‖ * HAdd.hAdd (α := ℝ) 1 1 - 2 * ε ≤ 2 * (‖T‖ - ε)
⊢ (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε ≤ ‖T‖ - ε

Tactic:
field_simp
-- 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT0 : ¬T = 0
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε
x : E
⊢ ‖T‖ * HAdd.hAdd (α := ℝ) 1 1 - 2 * ε ≤ 2 * (‖T‖ - ε)

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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT'' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
obtain :
  ∀ (ε : ℝ) (hε0 : ε > 0) (hε : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε),
    ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε
⊢ ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε

Tactic:
obtain ⟨ε, hε0, hε⟩ := T.rayleighQuotient_le_of_norm_mem_resolventSet hT'

Premises used: ContinuousLinearMap.rayleighQuotient_le_of_norm_mem_resolventSet
-- 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT'' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
⊢ Membership.mem (α := 𝕜) (resolventSet 𝕜 (-T)) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖-T‖ : 𝕜)

Tactic:
simpa [resolventSet_neg]

Premises used: resolventSet_neg
-- 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT'' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
obtain :
  ∀ (ε' : ℝ) (hε'0 : ε' > 0) (hε' : ∀ (x : E), (-T).rayleighQuotient x ≤ ‖-T‖ - ε'),
    ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε
⊢ ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε

Tactic:
obtain ⟨ε', hε'0, hε'⟩ := (-T).rayleighQuotient_le_of_norm_mem_resolventSet <| by
    simpa [resolventSet_neg]

Premises used: ContinuousLinearMap.rayleighQuotient_le_of_norm_mem_resolventSet, Neg.neg
-- 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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT'' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
ε' : ℝ
hε'0 : ε' > 0
hε' : ∀ (x : E), (-T).rayleighQuotient x ≤ ‖-T‖ - ε'
⊢ min ε ε' > 0

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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT'' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
ε' : ℝ
hε'0 : ε' > 0
hε' : ∀ (x : E), (-T).rayleighQuotient x ≤ ‖-T‖ - ε'
x : E
⊢ |T.rayleighQuotient x| ≤ ‖T‖ - min ε ε'

Tactic:
grind [rayleighQuotient_neg_apply, norm_neg]

Premises used: norm_neg, ContinuousLinearMap.rayleighQuotient_neg_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
inst_3 : Nontrivial E
hT' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
hT'' : Membership.mem (α := 𝕜) (resolventSet 𝕜 T) (-(algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖T‖ : 𝕜)
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
ε' : ℝ
hε'0 : ε' > 0
hε' : ∀ (x : E), (-T).rayleighQuotient x ≤ ‖-T‖ - ε'
⊢ ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε

Tactic:
exact ⟨min ε ε', by grind, fun x ↦ by grind [rayleighQuotient_neg_apply, norm_neg]⟩
-- 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
inst_3 : CompleteSpace E
hT : IsSelfAdjoint T
⊢ Nontrivial E

Tactic:
nontriviality E