awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M
have transitivity₁ : M * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4 ≤ M
Tactic: transitivity M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4
have 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⟫_𝕜) : 𝕜)) : ℝ)
Tactic: have key := congrArg re (add_conj ⟪T x, y⟫)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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⟫_𝕜) : 𝕜)) : ℝ)
⊢ (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, y⟫_𝕜 ≤ M * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4
have 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⟫_𝕜 : ℝ)
Tactic: rw [map_add, conj_inner_symm, ← coe_coe, ← hT, coe_coe, re_mul_ofReal, ofNat_re] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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 * (HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2) / 4 ≤ M
have rw : M * (2 * (HPow.hPow (α := ℝ) (β := ℕ) 1 2 + HPow.hPow (α := ℝ) (β := ℕ) 1 2)) / 4 ≤ M
Tactic: rw [parallelogram_law_with_norm 𝕜 x y, hx, hy]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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 : 𝕜)
⊢ ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c
have pos : ∀ (hT0 : T = 0),
  ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c
Tactic: by_cases hT0 : T = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c
have neg : ∀ (hT0 : ¬T = 0),
  ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c
Tactic: by_cases hT0 : T = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
have 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
Tactic: obtain ⟨c, hc0, hc⟩ := antilipschitzWith_iff_exists_mul_le_norm.mp
    (antilipschitz_of_isEmbedding _ (isHomeomorph_of_isUnit hT').isEmbedding)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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)
⊢ ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - c
have 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))
Tactic: refine ⟨min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t)), by positivity, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ 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))
have 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))
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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)
⊢ 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))
have 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))
Tactic: grw [this, min_le_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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))
⊢ 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))
have 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)
Tactic: grw [this, min_le_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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))
have neg : T.rayleighQuotient x ≤ (HPow.hPow (β := ℕ) t 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * t) - HPow.hPow (β := ℕ) c 2 / (2 * t)
Tactic: suffices T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - c ^ 2 / (2 * t) by
    grw [this, min_le_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ 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)
have 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)
Tactic: specialize hc x
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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)
⊢ 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)
have 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
Tactic: rw [← sq_le_sq₀ (by positivity) (by positivity), sub_apply, algebraMap_apply,
    norm_sub_sq (𝕜 := 𝕜), inner_re_symm] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ 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)
have 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
Tactic: grw [le_opNorm] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ 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)
have 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
Tactic: simp [inner_smul_right, norm_smul, abs_of_pos ht] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ 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)
have 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)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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‖ : 𝕜)
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
have pos : ∀ (hT0 : T = 0), ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
Tactic: by_cases hT0 : T = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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‖ - ε
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
have neg : ∀ (hT0 : ¬T = 0), ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
Tactic: by_cases hT0 : T = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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‖ - ε
have 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‖ - ε
Tactic: obtain ⟨ε, hε0, hε⟩ := T.rayleighQuotient_le_of_mem_resolventSet ‖T‖ (by positivity) hT'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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‖ - ε
have neg : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
Tactic: refine ⟨ε, hε0, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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.rayleighQuotient x ≤ ‖T‖ - ε
have neg : (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε ≤ ‖T‖ - ε
Tactic: grw [hε]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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
⊢ (HPow.hPow (β := ℕ) ‖T‖ 2 + HPow.hPow (β := ℕ) ‖T‖ 2) / (2 * ‖T‖) - ε ≤ ‖T‖ - ε
have neg : ‖T‖ * HAdd.hAdd (α := ℝ) 1 1 - 2 * ε ≤ 2 * (‖T‖ - ε)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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‖ : 𝕜)
⊢ ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε
have obtain : ∀ (ε : ℝ) (hε0 : ε > 0) (hε : ∀ (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'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
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‖ - ε
⊢ ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε
have obtain : ∀ (ε' : ℝ) (hε'0 : ε' > 0) (hε' : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (hypothesis)
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
⊢ spectralRadius 𝕜 T = (↑‖T‖₊ : ENNReal)
have a : Nontrivial E
Tactic: nontriviality E