Physicslib4.Spectral.Basic

Bounded operators on a Hilbert space: basic spectral prerequisites

This file collects the facts about a complex Hilbert space H and the algebra H →L[ℂ] H of bounded operators on it that the blueprint's section on spectral theorems (sctn:spectral-theorems) uses as prerequisites and which are not already available in Mathlib. Prerequisites that Mathlib does supply are recorded in the dictionary below rather than restated as local theorems.

Throughout, H is a complex Hilbert space, so that H →L[ℂ] H is the blueprint's 𝓑(H).

Main definitions

• Physicslib4.Spectral.BddMeasurable — the complex vector space of bounded measurable complex-valued functions on a measurable space. This is the single spelling of "bounded Borel function" used throughout the Spectral directory, in place of a repeated Measurable f ∧ ∃ K, ∀ x, ‖f x‖ ≤ K hypothesis pair.
• Physicslib4.Spectral.BoundedPointwiseLimit — "the sequence f is uniformly bounded by M and converges pointwise to g", the hypothesis package shared by every bounded-convergence and monotone-class argument in this directory.

Main statements

• Physicslib4.Spectral.mem_span_orthogonal_iff — the orthogonal complement of an arbitrary subset of H.
• Physicslib4.Spectral.completeSpace_boundedOp — 𝓑(H) is a Banach space.
• Physicslib4.Spectral.mem_resolventSet_iff_isUnit_sub_smul, Physicslib4.Spectral.spectrum_eq_compl_resolventSet, Physicslib4.Spectral.mul_resolvent_of_mem_resolventSet — the resolvent set, the spectrum, and the resolvent, in the blueprint's sign convention.
• Physicslib4.Spectral.riesz_representation — the Riesz representation theorem.
• Physicslib4.Spectral.norm_adjoint, Physicslib4.Spectral.norm_adjoint_mul_self — the C⋆-identities.
• Physicslib4.Spectral.adjoint_add, Physicslib4.Spectral.adjoint_smul, Physicslib4.Spectral.adjoint_mul, Physicslib4.Spectral.adjoint_pow, Physicslib4.Spectral.adjoint_one — the *-algebra identities for the adjoint.
• Physicslib4.Spectral.tendsto_adjoint — continuity of the adjoint.
• Physicslib4.Spectral.norm_apply_le_of_isStarProjection — projections are norm decreasing.
• Physicslib4.Spectral.opNorm_eq_sSup_inner — the operator norm as a supremum of matrix elements over pairs of unit vectors.
• Physicslib4.Spectral.continuous_iff_exists_bound — bounded ↔ continuous for linear maps between normed spaces.
• Physicslib4.Spectral.exists_simpleFunc_tendstoUniformly — a bounded measurable complex function is a uniform limit of simple functions.
• Physicslib4.Spectral.tendsto_iff_isBounded_of_monotone, Physicslib4.Spectral.tendsto_iff_isBounded_of_antitone — the monotone convergence theorem for real sequences.
• Physicslib4.Spectral.measurable_of_tendsto_pointwise, Physicslib4.Spectral.norm_le_of_tendsto — pointwise limits of uniformly bounded measurable functions.
• Physicslib4.Spectral.tendsto_integral_of_boundedPointwiseLimit — the bounded convergence theorem on a finite measure space.

Implementation notes

Mathlib's ContinuousLinearMap.adjoint supplies the blueprint's A ↦ A⋆, and IsStarProjection supplies the blueprint's bounded orthogonal projections; the blueprint's ρ(A), σ(A) are Mathlib's resolventSet ℂ A, spectrum ℂ A, noting that Mathlib uses λ • 1 - A where the blueprint uses A - λ • 1, which describes the same set (mem_resolventSet_iff_isUnit_sub_smul).

The blueprint's standing convention H ≠ {0}, stated in the section preamble alongside def:bounded-operator-notation, is localised, as the blueprint itself prescribes: it appears as a Nontrivial H hypothesis on exactly those declarations that use it. No declaration in this file needs it. The blueprint's other standing convention, separability of H (def:bounded-operator-notation), is never needed in this directory: the only place one might expect it — the convergence of the partial sums ∑_{i<n} Pᵢψ of a family of mutually annihilating projections in Physicslib4/Spectral/ProjectionValuedMeasure.lean — follows from ‖∑_{i<n} Pᵢψ‖² = ∑_{i<n} ‖Pᵢψ‖² ≤ ‖ψ‖² and completeness alone. Accordingly no declaration in the Spectral directory carries a SeparableSpace H hypothesis, and its absence is deliberate.

Blueprint conventions that are literally Mathlib declarations

The blueprint opens with a block of notational conventions and a proposition collecting standard facts. Each is exactly a Mathlib declaration, so it is cited rather than restated here; the blueprint nodes carry those Mathlib names.

• def:inner-product — Mathlib's InnerProductSpace ℂ H has precisely the blueprint's axioms, and conjugates the first argument, which is the blueprint's (physics) convention: inner_conj_symm, inner_self_im, inner_self_nonneg, inner_self_eq_zero, inner_smul_left, inner_smul_right, inner_add_left, inner_add_right.
• def:induced-norm — norm_eq_sqrt_re_inner.
• def:bounded-operator-notation — ContinuousLinearMap.le_opNorm and ContinuousLinearMap.opNorm_le_bound (the operator norm is the least bound); 𝓑(H) is H →L[ℂ] H.
• def:identity-operator — ContinuousLinearMap.norm_id, ContinuousLinearMap.one_def and ContinuousLinearMap.id_apply.
• def:indicator-function — Set.indicator, Set.indicator_apply, Set.indicator_of_mem, Set.indicator_of_notMem, Set.indicator_mul, Set.indicator_union_of_disjoint.
• def:identity-and-indicator — carried by Physicslib4.Spectral.one_apply_and_indicator_apply below, which asserts both halves of the compound anchor together and also records the convention that ℕ includes 0.
• prpstn:basic-integral-properties — MeasureTheory.integral_indicator, MeasureTheory.integral_add, MeasureTheory.integral_smul, MeasureTheory.lintegral_mono, norm_integral_le_integral_norm.
• prpstn:hall-a.43 (Cauchy–Schwarz) — norm_inner_le_norm and, in the squared form the blueprint states first, inner_mul_inner_self_le.
• prpstn:reverse-triangle-inequality — abs_norm_sub_norm_le.
• def:bounded-inverse — isUnit_iff_exists.
• def:adjoint-bounded — ContinuousLinearMap.eq_adjoint_iff (existence and uniqueness of the adjoint), ContinuousLinearMap.adjoint_inner_left, ContinuousLinearMap.star_eq_adjoint, ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.
• prpstn:hall-7.3 — ContinuousLinearMap.orthogonal_range. This is an equality of Submodules, (T : E →ₗ F).rangeᗮ = (T⋆).ker, rather than the blueprint's equality of subsets of H; the two are interchangeable through SetLike.ext_iff.
• prpstn:continuity-of-norm-and-inner-product — Filter.Tendsto.norm and Filter.Tendsto.inner.

The same holds of the analysis prerequisites the spectral section quotes from a functional-analysis course. Where the Mathlib spelling is not a literal transcription of the blueprint, the divergence is recorded.

• lmm:lemma-2 — norm_mul_le, applied through the NormedRing (H →L[ℂ] H) instance, in which A * B is composition. (ContinuousLinearMap.opNorm_comp_le is the same inequality written with ∘L.)
• prpstn:hall-a.34 — Summable.of_norm, whose ambient [CompleteSpace E] is exactly the blueprint's hypothesis that V is Banach; the comparison-test form used in practice is Summable.of_norm_bounded. Caveat: Mathlib's Summable is unconditional summability over the index type, which for a series indexed by ℕ in a Banach space is strictly stronger than convergence of the partial sums. This is harmless here, because the hypothesis ∑ ‖ψᵢ‖ < ∞ is absolute convergence, under which the two notions agree.
• lmm:nth-term-test — Summable.tendsto_atTop_zero, i.e. the blueprint's contrapositive form ∑ aᵢ converges ⇒ ‖aᵢ‖ → 0. Caveat: as above, the Lean hypothesis is unconditional Summable f, not mere convergence of the partial sums ∑_{i<n} aᵢ, so the Lean statement is formally weaker than the blueprint's; it is what every use in this section needs, since the series involved are all absolutely convergent.
• thrm:analytic-equivalence-theorem — Complex.analyticOnNhd_iff_differentiableOn (Complex.analyticOn_iff_differentiableOn for the AnalyticOn variant). Stated for Banach-space-valued f : ℂ → E, which covers the blueprint's scalar case.
• thrm:maximum-modulus-principle — Complex.exists_mem_frontier_isMaxOn_norm is the blueprint's statement itself (|f| attains its maximum at a point of the frontier), and Complex.norm_le_of_forall_mem_frontier_norm_le is the corollary form actually used downstream (a bound on the frontier propagates to the closure). Caveats: Mathlib's DiffContOnCl ℂ f U is the blueprint's "continuous on B̄, holomorphic on B"; and Mathlib drops the blueprint's hypothesis that B be connected, which is superfluous — the maximum modulus principle in this form holds on any bounded non-empty open set.
• thrm:hall-a.40 — banach_steinhaus, the principle of uniform boundedness; banach_steinhaus_iSup_nnnorm is the ℝ≥0∞-supremum variant.

Notation anchors

theorem Physicslib4.Spectral.one_apply_and_indicator_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {X : Type u_2} (E : Set X) (x : X) [Decidable (x ∈ E)] : (∀ (ψ : H), 1 ψ = ψ) ∧ E.indicator 1 x = if x ∈ E then 1 else 0

The compound anchor for the two notational conventions fixed together in the blueprint: the identity operator 1 acts as the identity on every vector, and the indicator function 1_E takes the value 1 on E and 0 off it.

This node also fixes a third convention with no propositional content, that ℕ = {0, 1, 2, ...} includes 0, matching Lean and Mathlib. Section 10.3 cites this anchor for that convention as well as for the two notations.

Blueprint reference: def:identity-and-indicator.

Orthogonal complements of subsets

theorem Physicslib4.Spectral.mem_span_orthogonal_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {V : Set H} {ψ : H} : ψ ∈ (Submodule.span ℂ V)ᗮ ↔ ∀ v ∈ V, inner ℂ ψ v = 0

The orthogonal complement of an arbitrary subset V ⊆ H is the orthogonal complement (Submodule.span ℂ V)ᗮ of the submodule it spans: a vector ψ lies in it exactly when ⟪ψ, v⟫ = 0 for every v ∈ V.

Blueprint reference: def:orthogonal-complement.

Bounded measurable functions

The blueprint's "bounded Borel function on X" is used as a hypothesis on roughly thirty declarations in this directory. We package it once, as a Submodule (the class is a complex vector space, which is how the blueprint uses it), rather than threading a Measurable f ∧ ∃ K, ∀ x, ‖f x‖ ≤ K pair through every signature.

def Physicslib4.Spectral.BddMeasurable (X : Type u_2) [MeasurableSpace X] : Submodule ℂ (X → ℂ)

The complex vector space of bounded measurable complex-valued functions on a measurable space X.

A function f : X → ℂ belongs to it when f is measurable and |f(x)| ≤ C for some constant C and every x ∈ X. On the spectrum of an operator, with its Borel σ-algebra, these are the bounded Borel functions to which the Borel functional calculus applies: indicator functions 1_E of Borel sets E (the spectral projections), step functions, and every bounded continuous function.

Implementation note: the class is a Submodule ℂ (X → ℂ), so membership packages the two hypotheses Measurable f and ∃ C, ∀ x, ‖f x‖ ≤ C (mem_bddMeasurable), and closure under sums and scalar multiples is part of the structure. It is the single spelling of "bounded Borel function" in the spectral files.

Blueprint: the bounded Borel functions of def:hall-8.8 and thrm:operator-valued-integration

Equations

• Physicslib4.Spectral.BddMeasurable X = { carrier := {f : X → ℂ | Measurable f ∧ ∃ (C : ℝ), ∀ (x : X), ‖f x‖ ≤ C}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Physicslib4.Spectral.mem_bddMeasurable {X : Type u_2} [MeasurableSpace X] {f : X → ℂ} : f ∈ BddMeasurable X ↔ Measurable f ∧ ∃ (C : ℝ), ∀ (x : X), ‖f x‖ ≤ C

theorem Physicslib4.Spectral.measurable_of_mem_bddMeasurable {X : Type u_2} [MeasurableSpace X] {f : X → ℂ} (hf : f ∈ BddMeasurable X) : Measurable f

theorem Physicslib4.Spectral.exists_bound_of_mem_bddMeasurable {X : Type u_2} [MeasurableSpace X] {f : X → ℂ} (hf : f ∈ BddMeasurable X) : ∃ (C : ℝ), ∀ (x : X), ‖f x‖ ≤ C

𝓑(H) as a Banach space

theorem Physicslib4.Spectral.completeSpace_boundedOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : CompleteSpace (H →L[ℂ] H)

𝓑(H) is a Banach space: it is a normed ℂ-algebra (the NormedRing and NormedAlgebra instances on H →L[ℂ] H) and it is complete in the operator norm. Only completeness has propositional content, so it is what is stated here.

Blueprint reference: lmm:bounded-operators-form-a-banach-space.

The resolvent set, the spectrum and the resolvent

Mathlib's resolventSet ℂ A is defined through λ𝟙 - A, whereas the blueprint uses A - λ𝟙; since -1 is a unit these describe the same set, which is the content of mem_resolventSet_iff_isUnit_sub_smul.

Blueprint reference: def:bounded-operator-resolvent-and-spectrum.

theorem Physicslib4.Spectral.mem_resolventSet_iff_isUnit_sub_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) (lam : ℂ) : lam ∈ resolventSet ℂ A ↔ IsUnit (A - lam • 1)

A complex number λ lies in the resolvent set ρ(A) exactly when A − λ𝟙 has a bounded inverse.

The resolvent set of a bounded operator A is the set of λ ∈ ℂ for which A − λ𝟙 is invertible in the algebra of bounded operators, that is, has a two-sided inverse that is again bounded. The statement identifies Mathlib's resolvent set with that definition.

Implementation note: Mathlib's resolventSet ℂ A is defined through λ𝟙 − A (spectrum.mem_resolventSet_iff); this theorem converts to the sign A − λ𝟙 by multiplying with the unit −1.

Blueprint: def:bounded-operator-resolvent-and-spectrum

theorem Physicslib4.Spectral.spectrum_eq_compl_resolventSet {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) : spectrum ℂ A = (resolventSet ℂ A)ᶜ

The spectrum σ(A) of a bounded operator A is the complement of its resolvent set ρ(A).

So λ ∈ σ(A) exactly when A − λ𝟙 has no bounded inverse. Every eigenvalue lies in the spectrum, but in infinite dimensions the spectrum can contain more: for a multiplication operator (Mψ)(x) = xψ(x) on L²([0, 1]) it is all of [0, 1], although M has no eigenvalues.

Implementation note: Mathlib's spectrum ℂ A is by definition the complement of resolventSet ℂ A, so the proof is rfl.

Blueprint: def:bounded-operator-resolvent-and-spectrum

theorem Physicslib4.Spectral.mul_resolvent_of_mem_resolventSet {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) {lam : ℂ} (h : lam ∈ resolventSet ℂ A) : (lam • 1 - A) * resolvent A lam = 1

For λ in the resolvent set, Mathlib's resolvent A λ is a right inverse of λ𝟙 − A.

Implementation note: Mathlib's resolvent A λ is the inverse of λ𝟙 − A, so it is the negative of the blueprint's resolvent (A − λ𝟙)⁻¹. This project states only the right-inverse equation.

Blueprint: the resolvent of def:bounded-operator-resolvent-and-spectrum

The Riesz representation theorem

theorem Physicslib4.Spectral.riesz_representation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ξ : H →L[ℂ] ℂ) : ∃! χ : H, (∀ (ψ : H), ξ ψ = inner ℂ χ ψ) ∧ ‖χ‖ = ‖ξ‖

The Riesz representation theorem: every bounded linear functional on H is ψ ↦ ⟪χ, ψ⟫ for a unique χ ∈ H, whose norm is the operator norm of the functional. Mathlib packages this as the conjugate-linear isometric equivalence InnerProductSpace.toDual.

Blueprint reference: thrm:hall-a.52.

The adjoint

The defining property of the adjoint and its uniqueness are Mathlib's ContinuousLinearMap.eq_adjoint_iff (blueprint def:adjoint-bounded). What is recorded here are the facts Mathlib does not state in this form: the two C⋆-identities, the *-algebra identities, and continuity.

theorem Physicslib4.Spectral.norm_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) : ‖ContinuousLinearMap.adjoint A‖ = ‖A‖

The adjoint is norm preserving; in particular A⋆ is again a bounded operator, and ‖A⋆‖ ≤ ‖A‖.

Blueprint references: prpstn:adjoint-is-bounded and the first half of prpstn:hall-7.2.

theorem Physicslib4.Spectral.norm_adjoint_mul_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) : ‖ContinuousLinearMap.adjoint A * A‖ = ‖A‖ ^ 2

The C⋆-identity ‖A⋆A‖ = ‖A‖² on 𝓑(H).

Blueprint reference: prpstn:hall-7.2 (second half).

theorem Physicslib4.Spectral.adjoint_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A B : H →L[ℂ] H) : ContinuousLinearMap.adjoint (A + B) = ContinuousLinearMap.adjoint A + ContinuousLinearMap.adjoint B

The adjoint is additive.

Blueprint reference: lmm:adjoint-algebra.

theorem Physicslib4.Spectral.adjoint_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : ℂ) (A : H →L[ℂ] H) : ContinuousLinearMap.adjoint (c • A) = (starRingEnd ℂ) c • ContinuousLinearMap.adjoint A

The adjoint is conjugate homogeneous.

Blueprint reference: lmm:adjoint-algebra.

theorem Physicslib4.Spectral.adjoint_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A B : H →L[ℂ] H) : ContinuousLinearMap.adjoint (A * B) = ContinuousLinearMap.adjoint B * ContinuousLinearMap.adjoint A

The adjoint is anti-multiplicative.

Blueprint reference: lmm:adjoint-algebra.

theorem Physicslib4.Spectral.adjoint_pow {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (k : ℕ) : ContinuousLinearMap.adjoint (A ^ k) = ContinuousLinearMap.adjoint A ^ k

The adjoint is compatible with powers.

Blueprint reference: lmm:adjoint-algebra.

theorem Physicslib4.Spectral.adjoint_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : ContinuousLinearMap.adjoint 1 = 1

The adjoint fixes the identity operator. (Involutivity of the adjoint is Mathlib's ContinuousLinearMap.adjoint_adjoint.)

Blueprint reference: lmm:adjoint-algebra.

theorem Physicslib4.Spectral.tendsto_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {B : ℕ → H →L[ℂ] H} {B₀ : H →L[ℂ] H} (h : Filter.Tendsto B Filter.atTop (nhds B₀)) : Filter.Tendsto (fun (n : ℕ) => ContinuousLinearMap.adjoint (B n)) Filter.atTop (nhds (ContinuousLinearMap.adjoint B₀))

Convergence in the operator norm is preserved by taking adjoints.

Blueprint reference: prpstn:continuity-of-the-adjoint.

Orthogonal projections

theorem Physicslib4.Spectral.norm_apply_le_of_isStarProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (hP : IsStarProjection P) (ψ : H) : ‖P ψ‖ ≤ ‖ψ‖

A bounded orthogonal projection is norm decreasing.

Blueprint reference: lmm:projection-norm-decreasing.

The operator norm

theorem Physicslib4.Spectral.opNorm_eq_sSup_inner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) : ‖A‖ = sSup {r : ℝ | ∃ (χ : H) (ψ : H), ‖χ‖ = 1 ∧ ‖ψ‖ = 1 ∧ r = ‖inner ℂ χ (A ψ)‖}

The operator norm of A is the supremum of the moduli of its matrix elements ⟪χ, A ψ⟫ over pairs of unit vectors.

Blueprint reference: lmm:lemma-1.

theorem Physicslib4.Spectral.continuous_iff_exists_bound {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℂ E] [NormedSpace ℂ F] (T : E →ₗ[ℂ] F) : Continuous ⇑T ↔ ∃ (C : ℝ), ∀ (x : E), ‖T x‖ ≤ C * ‖x‖

A linear map between normed spaces is bounded if and only if it is continuous.

Blueprint reference: prpstn:bounded-operators-are-continuous.

Approximation and convergence prerequisites

theorem Physicslib4.Spectral.exists_simpleFunc_tendstoUniformly {X : Type u_2} [MeasurableSpace X] {f : X → ℂ} (hf : f ∈ BddMeasurable X) : ∃ (s : ℕ → MeasureTheory.SimpleFunc X ℂ), TendstoUniformly (fun (n : ℕ) (x : X) => (s n) x) f Filter.atTop

The complex-valued simple approximation theorem: a bounded measurable complex-valued function on a measurable space is the uniform limit of a sequence of simple functions.

Mathlib's MeasureTheory.StronglyMeasurable.approxBounded gives an almost everywhere pointwise approximation by bounded simple functions; the uniform statement below is genuinely stronger and is proved by slicing the (bounded) range of f into finitely many pieces of diameter < 1/n.

Blueprint reference: thrm:complex-valued-simple-approximation-theorem.

theorem Physicslib4.Spectral.tendsto_iff_isBounded_of_monotone {a : ℕ → ℝ} (ha : Monotone a) : (∃ (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L)) ↔ Bornology.IsBounded (Set.range a)

The monotone convergence theorem for real sequences: a monotone sequence of reals has a finite limit if and only if it is bounded.

Blueprint reference: thrm:monotone-convergence-theorem.

theorem Physicslib4.Spectral.tendsto_iff_isBounded_of_antitone {a : ℕ → ℝ} (ha : Antitone a) : (∃ (L : ℝ), Filter.Tendsto a Filter.atTop (nhds L)) ↔ Bornology.IsBounded (Set.range a)

The monotone convergence theorem for real sequences, decreasing case.

Blueprint reference: thrm:monotone-convergence-theorem.

Uniformly bounded pointwise limits

Almost every convergence argument in this directory — the extension of the functional calculus from continuous to bounded Borel functions, the monotone-class bootstrap, and the bounded convergence theorem for the measures μ_ψ — feeds on the same package of hypotheses on a sequence f : ℕ → α → ℂ: a single bound M valid for all indices and all points, plus pointwise convergence to a limit g. It is named once here and reused, rather than respelled as a pair of binders in each signature.

structure Physicslib4.Spectral.BoundedPointwiseLimit {α : Type u_2} (f : ℕ → α → ℂ) (g : α → ℂ) (b : α → ℝ) : Prop

A sequence of functions f_n : α → ℂ is bounded by b uniformly in n and converges pointwise to g.

The hypotheses are |f_n(x)| ≤ b(x) for every n and every x, and f_n(x) → g(x) for every x. The convergence is pointwise, not uniform: its rate may depend on the point. This is the hypothesis of the bounded convergence theorem (tendsto_integral_of_boundedPointwiseLimit), which extends the functional calculus from continuous to bounded Borel functions.

Implementation note: the bound b is usually a constant fun _ => M; it may vary so that the same predicate covers the quadratic bound fun φ => C * ‖φ‖ ^ 2 for sequences of quadratic forms in Physicslib4/Spectral/Forms.lean.

Blueprint: the hypotheses of thrm:bounded-convergence-theorem

• norm_le (n : ℕ) (x : α) : ‖f n x‖ ≤ b x

  The sequence is dominated by b, uniformly in the index.

• tendsto (x : α) : Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))

  The sequence converges to g pointwise.

theorem Physicslib4.Spectral.measurable_of_tendsto_pointwise {X : Type u_2} [MeasurableSpace X] {f : ℕ → X → ℂ} {g : X → ℂ} (hmeas : ∀ (i : ℕ), Measurable (f i)) (hlim : ∀ (x : X), Filter.Tendsto (fun (i : ℕ) => f i x) Filter.atTop (nhds (g x))) : Measurable g

A pointwise limit of measurable complex-valued functions is measurable.

Blueprint reference: lmm:pointwise-limits-of-borel-measurable-functions (first half).

theorem Physicslib4.Spectral.norm_le_of_tendsto {α : Type u_2} {f : ℕ → α → ℂ} {g : α → ℂ} {b : α → ℝ} (h : BoundedPointwiseLimit f g b) (x : α) : ‖g x‖ ≤ b x

A pointwise limit of a uniformly bounded sequence of functions obeys the same bound.

Blueprint reference: lmm:pointwise-limits-of-borel-measurable-functions (second half).

theorem Physicslib4.Spectral.tendsto_integral_of_boundedPointwiseLimit {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → X → ℂ} {g : X → ℂ} {M : ℝ} (hmeas : ∀ (i : ℕ), Measurable (f i)) (h : BoundedPointwiseLimit f g fun (x : X) => M) : Filter.Tendsto (fun (i : ℕ) => ∫ (x : X), f i x ∂μ) Filter.atTop (nhds (∫ (x : X), g x ∂μ))

The bounded convergence theorem: on a space of finite measure, the integrals of a uniformly bounded sequence of measurable complex-valued functions converge to the integral of its pointwise limit.

This is the constant-dominating-function case of Mathlib's MeasureTheory.tendsto_integral_of_dominated_convergence; the constant is integrable precisely because μ is finite, which is the blueprint's hypothesis μ(X) < ∞. Measurability of each f i is carried explicitly: the blueprint leaves it implicit in writing ∫_X f_i dμ, but the integral is only defined with it.

Blueprint reference: thrm:bounded-convergence-theorem.