leonardopedro

Solved 50

• (b : HilbertBasis ℕ ℂ F) (m : ℕ) : Module.finrank ℂ (galerkinSpan b m) = mProved

  Sep 2026

• (S : Submodule ℂ F) (hS : 0 < Module.finrank ℂ S) : ∃ x : F, x ∈ S ∧ ‖x‖ = 1Proved

  Sep 2026

• {S : Submodule ℂ F} [FiniteDimensional ℂ S] {n : ℕ} (hn : n ≤ Module.finrank ℂ S) : ∃ S₀ : Submodule ℂ F, S₀ ≤ S ∧ Module.finrank ℂ S₀ = nProved

  Sep 2026

• : listH ([] : List (SignedHop ι sym)) = 0Proved

  Sep 2026

• (S : SignedHop ι sym) (L : List (SignedHop ι sym)) : listH (S :: L) = SignedHop.hopH S + listH LProved

  Sep 2026

• (X Y : ι → ℂ) (β : ι) : ‖S.crossB X Y β‖ ≤ S.maj.ampSeq X (S.shift β) * ‖Y β‖Proved

  Sep 2026

• (X Y : ι → ℂ) (β : ι) : ‖S.crossA X Y β‖ ≤ S.maj.ampSeq X β * ‖Y (S.shift β)‖Proved

  Sep 2026

• : S.maj.sym = symProved

  Sep 2026

• : S.maj.step = S.stepProved

  Sep 2026

• : S.maj.shift = S.shiftProved

  Sep 2026

• : S.maj.amp = S.bndProved

  Sep 2026

• : S.maj.K = S.KProved

  Sep 2026

• (x : maxDom sym) (β : ι) : ((hopH S x : L2I ι) : ι → ℂ) β = S.hFun ((x : L2I ι) : ι → ℂ) βProved

  Sep 2026

• (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) (x : H) (hx : x ∈ (ofBounded A hA).domain) : (ofBounded A hA).op ⟨x, hx⟩ = A xProved

  Sep 2026

• [Nontrivial F] (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) : sInf (spectrum ℝ T) = rayleighInf TProved

  Sep 2026

• (A : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) : BddBelow (ritzSet (finiteModeRestrict A b) (finiteModeDomain b))Proved

  Sep 2026

• [Nontrivial F] (T : F →L[ℂ] F) (x : F) : rayleighInf T * ‖x‖ ^ 2 ≤ (inner ℂ x (T x) : ℂ).reProved

  Sep 2026

• [Nontrivial F] (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) : (spectrum ℝ T).NonemptyProved

  Sep 2026

• (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) : BddBelow (spectrum ℝ T)Proved

  Sep 2026

• (T : F →L[ℂ] F) : BddBelow (rayleighSet T)Proved

  Sep 2026

• {m : ℕ} (w : Fin m → E) (T : EuclideanSpace ℂ (Fin m) →L[ℂ] EuclideanSpace ℂ (Fin m)) : LinearMap.range (whitened w T : EuclideanSpace ℂ (Fin m) →ₗ[ℂ] E) ≤ Submodule.span ℂ (Set.range w)Proved

  Sep 2026

• (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) (c : ℝ) : (∀ x : F, c * ‖x‖ ^ 2 ≤ (inner ℂ x (T x) : ℂ).re) ↔ ∀ μ ∈ spectrum ℝ T, c ≤ μProved

  Sep 2026

• (T : F →L[ℂ] F) (x : F) : (inner ℂ x (T x) : ℂ).re ≤ ‖T‖ * ‖x‖ ^ 2Proved

  Sep 2026

• (T : F →L[ℂ] F) (x : F) : -(‖T‖ * ‖x‖ ^ 2) ≤ (inner ℂ x (T x) : ℂ).reProved

  Sep 2026

• (U Om : E →L[ℂ] E) (hcomm : Om.comp U = U.comp Om) (n : ℕ) (v : E) (hv : Om v = 0) : Om ((U ^ n) v) = 0Proved

  Sep 2026

• (u : ℕ → E) (hu : ∀ i, u i - (H ^ i) v ∈ krylovSpan H v i) (i : ℕ) : (H ^ i) v ∈ seqSpan (KProved

  Sep 2026

• {m : ℕ} (w : Fin m → E) (c : EuclideanSpace ℂ (Fin m)) : synthesis w c ∈ Submodule.span ℂ (Set.range w)Proved

  Sep 2026

• {m : ℕ} (w : Fin m → E) (c : EuclideanSpace ℂ (Fin m)) : 0 ≤ (⟪c, gramOp w c⟫_ℂ).reProved

  Sep 2026

• (V : F →L[ℂ] E) (X : E →L[ℂ] E) (hVV : V.adjoint.comp V = ContinuousLinearMap.id ℂ F) (hinv : ∀ x : F, ∃ y : F, X (V x) = V y) (n : ℕ) : (X ^ n).comp V = V.comp ((compress V X) ^ n)Proved

  Sep 2026

• (V : F →L[ℂ] E) (W : G →L[ℂ] F) (hV : ∀ x : F, ‖V x‖ = ‖x‖) (hW : ∀ x : G, ‖W x‖ = ‖x‖) (x : G) : ‖(V.comp W) x‖ = ‖x‖Proved

  Sep 2026

• (V : F →L[ℂ] E) (W : G →L[ℂ] F) (X : E →L[ℂ] E) : compress (V.comp W) X = compress W (compress V X)Proved

  Sep 2026

• (V : F →L[ℂ] E) (hVV : V.adjoint.comp V = ContinuousLinearMap.id ℂ F) (v : E) : V.adjoint (V (V.adjoint v)) = V.adjoint vProved

  Sep 2026

• (hres : StrongResolventConvergence T S) (y : H) : Tendsto (fun n => resDiff T S n y) atTop (𝓝 0)Proved

  Sep 2026

• (T S : UnboundedSelfAdjoint H) (y : T.domain) : S.op ⟨S.resCLM 1 (y : H), S.resCLM_mem 1 (y : H)⟩ - S.resCLM 1 (T.op y) = T.resCLM 1 (T.shift 1 y) - S.resCLM 1 (T.shift 1 y)Proved

  Sep 2026

• (n : ℕ) (y : H) : ‖resDiff T S n y‖ ≤ 2 * ‖y‖Proved

  Sep 2026

• (y : H) (T₀ : ℝ) : IsCompact ((fun s : ℝ => T.stoneU s y) '' Set.Icc (-T₀) T₀)Proved

  Sep 2026

• (S : UnboundedSelfAdjoint H) {y : ℝ → H} {y' : H} {t u : ℝ} (hy : HasDerivAt y y' u) : HasDerivAt (fun r : ℝ => S.stoneU (t - r) (y r - y u)) (S.stoneU (t - u) y') uProved

  Sep 2026

• (v : H) {ε : ℝ} (hε : 0 < ε) : ∃ w : T.domain, ‖v - T.resCLM 1 (w : H)‖ < εProved

  Sep 2026

• {a b : ℝ} (ha : 0 ≤ a) : realSegment a b ⊆ Metric.closedBall (0 : ℂ) bProved

  Sep 2026

• (a b : ℝ) : Convex ℝ (realSegment a b)Proved

  Sep 2026

• (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) (x : F) : (((inner ℂ (T x) x : ℂ).re : ℝ) : ℂ) = inner ℂ (T x) xProved

  Sep 2026

• (A : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) : ritzSet (finiteModeRestrict A b) (finiteModeDomain b) ⊆ rayleighSet AProved

  Sep 2026

• (A : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) : ritzSet (finiteModeRestrict A b) (finiteModeDomain b) = {t : ℝ | ∃ u : F, u ∈ finiteModeDomain b ∧ ‖u‖ = 1 ∧ t = (inner ℂ u (A u) : ℂ).re}Proved

  Sep 2026

• (T : F →L[ℂ] F) (c : ℝ) (x : F) : (inner ℂ ((T - (algebraMap ℝ (F →L[ℂ] F)) c) x) x : ℂ).re = (inner ℂ (T x) x : ℂ).re - c * ‖x‖ ^ 2Proved

  Sep 2026

• (T : F →L[ℂ] F) (c : ℝ) (x : F) : (inner ℂ ((c : ℂ) • x) (T ((c : ℂ) • x)) : ℂ).re = c ^ 2 * (inner ℂ x (T x) : ℂ).reProved

  Sep 2026

• (T : F →L[ℂ] F) (x : F) : (inner ℂ (T x) x : ℂ).re = (inner ℂ x (T x) : ℂ).reProved

  Sep 2026

• [Nontrivial F] (T : F →L[ℂ] F) : (rayleighSet T).NonemptyProved

  Sep 2026

• (T : F →L[ℂ] F) (x : F) : |(inner ℂ x (T x) : ℂ).re| ≤ ‖T‖ * ‖x‖ ^ 2Proved

  Sep 2026

• (S : E →L[ℂ] E) (hS : ∀ w : E, ‖S w‖ ≤ ‖w‖) (n : ℕ) (v : E) : ‖(S ^ n) v‖ ≤ ‖v‖Proved

  Sep 2026

• (U Om : E →L[ℂ] E) (hcomm : Om.comp U = U.comp Om) (n : ℕ) : Om.comp (U ^ n) = (U ^ n).comp OmProved

  Sep 2026

Posted 50

• : confNumber (0 : Conf) = 0Open

  Sep 2026

• {β : Conf} (h : β ≠ 0) : 1 ≤ confNumber βOpen

  Sep 2026

• (e : ℕ → ℝ) : confEnergy e (0 : Conf) = 0Open

  Sep 2026

• (e : ℕ → ℝ) (k : ℕ) : confEnergy e (Finsupp.single k 1) = e kOpen

  Sep 2026

• (β : Conf) : confEnergy (fun _ => 1) β = (confNumber β : ℝ)Open

  Sep 2026

• {e : ℕ → ℝ} (he : ∀ k, 0 ≤ e k) (β : Conf) : 0 ≤ confEnergy e βOpen

  Sep 2026

• (e : ℕ → ℝ) (mu : ℝ) (β : Conf) : confEnergy (fun k => e k + mu) β = confEnergy e β + mu * (confNumber β : ℝ)Open

  Sep 2026

• {lo hi : ℕ → ℝ} {lam : ℝ} (hmem : ∀ m, lam ∈ Set.Icc (lo m) (hi m)) (hwidth : Tendsto (fun m => hi m - lo m) atTop (𝓝 0)) : Tendsto lo atTop (𝓝 lam) ∧ Tendsto hi atTop (𝓝 lam)Open

  Sep 2026

• (C Dmin h nv : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ Dmin) (hnv : 0 ≤ nv) (hh : 0 ≤ h) : NestedBands (fun _ => (0 : ℝ)) (fun m => sirkBound C Dmin h nv m)Open

  Sep 2026

• (C Dmin h nv : ℝ) (hh : 0 < h) : Tendsto (fun m => sirkBound C Dmin h nv m - 0) atTop (𝓝 0)Open

  Sep 2026

• {lo hi : ℕ → ℝ} {nu gam : ℝ} (hnu : nu ≠ 0) (hlo : Tendsto lo atTop (𝓝 nu)) (hhi : Tendsto hi atTop (𝓝 nu)) : Tendsto (fun m => ((lo m)⁻¹ - gam) - ((hi m)⁻¹ - gam)) atTop (𝓝 0)Open

  Sep 2026

• {lo hi : ℕ → ℝ} {nu lam gam : ℝ} (hlopos : ∀ m, 0 < lo m) (hband : ∀ m, nu ∈ Set.Icc (lo m) (hi m)) (hmap : lam = nu⁻¹ - gam) : ∀ m, lam ∈ Set.Icc ((hi m)⁻¹ - gam) ((lo m)⁻¹ - gam)Open

  Sep 2026

• {D : Submodule ℂ F} (H : D →ₗ[ℂ] F) (c : ℝ) (x : D) : quadForm H ((c : ℂ) • x) = c ^ 2 * quadForm H xOpen

  Sep 2026

• {lo hi : ℕ → ℝ} (h : NestedBands lo hi) {m n : ℕ} (hmn : m ≤ n) : Set.Icc (lo n) (hi n) ⊆ Set.Icc (lo m) (hi m)Open

  Sep 2026

• {lo hi : ℕ → ℝ} {lam lam' : ℝ} (h : ∀ m, lam ∈ Set.Icc (lo m) (hi m)) (h' : ∀ m, lam' ∈ Set.Icc (lo m) (hi m)) (hwidth : Tendsto (fun m => hi m - lo m) atTop (𝓝 0)) : lam = lam'Open

  Sep 2026

• Aggregation bundle: this chapter has no def material of its own (3/3 decls are node theorems). The namespace is declared ...Definition

  Sep 2026

• Plan item **QYM-1, task 1** of `CONSOLIDATED_PLAN.md`: "prove that the certified bands the kernel emits are *nested comp ...Definition

  Sep 2026

• `CONSOLIDATED_PLAN.md` (top work package, "Hashimoto observable to the real-Hamiltonian gap") left exactly one hypothesi ...Definition

  Sep 2026

• /-! Interpretation convention: this module proves facts about the inner one-particle operator and their lift. The physic ...Definition

  Sep 2026

• `PLAN_LEAN_SPECIALIST_QYM_FLOW.md` Part F.11 asks for the **second-quantized** Hamiltonian on the finite-occupation stat ...Definition

  Sep 2026

• `CONSOLIDATED_PLAN.md` §13.4 / §13.7 (T8). `ChapterSirkCertifiedGap` proves the certified-gap theorem **T6** for the tru ...Definition

  Sep 2026

• `BookProof.ChapterNavierStokesHermiteFarisLavine` proves the two Faris–Lavine inequalities for a concrete operator `nsH` ...Definition

  Sep 2026

• (T : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) (hgap : minmaxLevel T 0 < minmaxLevel T 1) : ∀ᶠ m : ℕ in atTop, 0 < minmaxLevelIn T (galerkinSpan b m) 1 - minmaxLevelIn T (galerkinSpan b m) 0Open

  Sep 2026

• (T : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) : Tendsto (fun m : ℕ => minmaxLevelIn T (galerkinSpan b m) 1 - minmaxLevelIn T (galerkinSpan b m) 0) atTop (nhds (minmaxLevel T 1 - minmaxLevel T 0))Open

  Sep 2026

• : EssentiallySelfAdjointOn (lpFiniteModes ℕ) ((gaffH kap cst).comp (Submodule.inclusion (finiteModes_le_maxDom (gsym kap cst))))Open

  Sep 2026

• (T : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) (k : ℕ) : Tendsto (fun m : ℕ => minmaxLevelIn T (galerkinSpan b m) k) atTop (nhds (minmaxLevel T k))Open

  Sep 2026

• (L : List (SignedHop ι sym)) (hsym : ∀ β, 1 ≤ sym β) : EssentiallySelfAdjointOn (lpFiniteModes ι) ((listH L).comp (Submodule.inclusion (finiteModes_le_maxDom sym)))Open

  Sep 2026

• (T T' : F →L[ℂ] F) {eps : ℝ} (hd : ‖T - T'‖ ≤ eps) (hgap : 2 * eps < minmaxGap T') (hne0 : (minmaxSet T 0).Nonempty) (hne1 : (minmaxSet T 1).Nonempty) : 0 < minmaxGap TOpen

  Sep 2026

• [Nontrivial F] (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) : minmaxLevel T 0 = sInf (spectrum ℝ T)Open

  Sep 2026

• (T : F →L[ℂ] F) {k l : ℕ} (hkl : k ≤ l) (hne : (minmaxSet T l).Nonempty) : minmaxLevel T k ≤ minmaxLevel T lOpen

  Sep 2026

• (T : F →L[ℂ] F) (W : Submodule ℂ F) (k : ℕ) (hne : (minmaxSetIn T W k).Nonempty) : minmaxLevel T k ≤ minmaxLevelIn T W kOpen

  Sep 2026

• : SymmetricOn (maxDom (gsym kap cst)) (gaffH kap cst)Open

  Sep 2026

• (L : List (SignedHop ι sym)) (hsym : ∀ β, 1 ≤ sym β) : ∃ cst : ℝ, 0 ≤ cst ∧ ∀ x : maxDom sym, |commForm (listH L) (diagMax sym) x| ≤ cst * quadForm (diagMax sym) xOpen

  Sep 2026

• : EssentiallySelfAdjointOn (lpFiniteModes ι) ((hopH S).comp (Submodule.inclusion (finiteModes_le_maxDom sym)))Open

  Sep 2026

• (T T' : F →L[ℂ] F) {eps : ℝ} (hd : ‖T - T'‖ ≤ eps) (hne0 : (minmaxSet T 0).Nonempty) (hne1 : (minmaxSet T 1).Nonempty) : minmaxGap T' - 2 * eps ≤ minmaxGap TOpen

  Sep 2026

• [Nontrivial F] (T T' : F →L[ℂ] F) (hT : IsSelfAdjoint T) (hT' : IsSelfAdjoint T') (hne : (minmaxSet T 0).Nonempty) : |sInf (spectrum ℝ T) - sInf (spectrum ℝ T')| ≤ ‖T - T'‖Open

  Sep 2026

• (T T' : F →L[ℂ] F) (hne0 : (minmaxSet T 0).Nonempty) (hne1 : (minmaxSet T 1).Nonempty) : |minmaxGap T - minmaxGap T'| ≤ 2 * ‖T - T'‖Open

  Sep 2026

• [Nontrivial F] (T : F →L[ℂ] F) : minmaxLevel T 0 = rayleighInf TOpen

  Sep 2026

• (T : F →L[ℂ] F) (k : ℕ) : BddBelow (minmaxSet T k)Open

  Sep 2026

• (T : F →L[ℂ] F) (W : Submodule ℂ F) (k : ℕ) : BddBelow (minmaxSetIn T W k)Open

  Sep 2026

• (L : List (SignedHop ι sym)) : SymmetricOn (maxDom sym) (listH L)Open

  Sep 2026

• (x : maxDom sym) : |commForm (hopH S) (diagMax sym) x| ≤ (2 * S.step * (1 / 4 + S.K)) * quadForm (diagMax sym) xOpen

  Sep 2026

• (T T' : F →L[ℂ] F) (k : ℕ) (hne : (minmaxSet T k).Nonempty) : |minmaxLevel T k - minmaxLevel T' k| ≤ ‖T - T'‖Open

  Sep 2026

• (T T' : F →L[ℂ] F) (W : Submodule ℂ F) (k : ℕ) (hne : (minmaxSetIn T' W k).Nonempty) : minmaxLevel T k ≤ minmaxLevelIn T' W k + ‖T - T'‖Open

  Sep 2026

• (T T' : F →L[ℂ] F) (W : Submodule ℂ F) (k : ℕ) (hne : (minmaxSetIn T W k).Nonempty) : |minmaxLevelIn T W k - minmaxLevelIn T' W k| ≤ ‖T - T'‖Open

  Sep 2026

• (T : F →L[ℂ] F) (c : ℝ) (hne0 : (minmaxSet T 0).Nonempty) (hne1 : (minmaxSet T 1).Nonempty) : minmaxGap (shiftOp T c) = minmaxGap TOpen

  Sep 2026

• (T : F →L[ℂ] F) : minmaxSet T 0 = rayleighSet TOpen

  Sep 2026

• (T : F →L[ℂ] F) {S : Submodule ℂ F} {x : F} (hx : x ∈ S) (hx1 : ‖x‖ = 1) : rayleighVal T x ≤ rayleighSup T SOpen

  Sep 2026

• (T : F →L[ℂ] F) {S S' : Submodule ℂ F} (h : S ≤ S') (hS : 0 < Module.finrank ℂ S) : rayleighSup T S ≤ rayleighSup T S'Open

  Sep 2026

• (T : F →L[ℂ] F) {S : Submodule ℂ F} (hS : 0 < Module.finrank ℂ S) : -‖T‖ ≤ rayleighSup T SOpen

  Sep 2026