Physicslib4.Spectral.BorelClasses

Bootstrapping from continuous to bounded Borel functions

The blueprint extends the continuous functional calculus to bounded Borel functions by a monotone-class argument: any class of bounded measurable functions which is a complex subspace, contains the continuous real functions, and is closed under uniformly bounded pointwise limits, already contains all bounded Borel functions.

This file records that argument's ingredients: bump functions, the monotone class theorem, the class L₀ of sets whose indicator is a bounded pointwise limit of continuous functions, and the class 𝒞 of the bootstrap itself.

Main definitions

• Physicslib4.Spectral.IsBumpFunction.
• Physicslib4.Spectral.IsMonotoneClass.
• Physicslib4.Spectral.L0 — the blueprint's 𝓛₀.
• Physicslib4.Spectral.IsBorelGenerating — the blueprint's hypotheses on 𝒞.

Main statements

• Physicslib4.Spectral.exists_isBumpFunction — Urysohn-type existence of bump functions on a normal space.
• Physicslib4.Spectral.generateFrom_subset_of_isMonotoneClass — the monotone class theorem.
• Physicslib4.Spectral.empty_mem_L0, Physicslib4.Spectral.compl_mem_L0, Physicslib4.Spectral.union_mem_L0, Physicslib4.Spectral.isClosed_mem_L0 — the closure properties of 𝓛₀. Only the last needs the metric; the variable blocks below are split accordingly.
• Physicslib4.Spectral.isSetAlgebra_L0 — 𝓛₀ is an algebra of sets containing the open sets, derived from the four preceding statements.
• Physicslib4.Spectral.IsBorelGenerating.indicator_mem — 𝒞 contains the indicator of every Borel set. Together with Physicslib4.Spectral.IsBorelGenerating.eq_bddMeasurable this is the only place the metric Borel context (no compactness) is needed; IsBorelGenerating itself is stated for an arbitrary topological measurable space.
• Physicslib4.Spectral.IsBorelGenerating.eq_bddMeasurable — 𝒞 is exactly the set of bounded Borel functions.

Implementation notes

The blueprint's def:algebra-of-sets is Mathlib's MeasureTheory.IsSetAlgebra.

Bump functions

structure Physicslib4.Spectral.IsBumpFunction {X : Type u_1} [TopologicalSpace X] (E U : Set X) (f : C(X, ℝ)) : Prop

A bump function for E inside U: a continuous f : X → [0, 1] with f = 1 on E and support in U.

Here E is meant to be closed and U an open set containing it. Bump functions are the continuous approximations to indicator functions: for a closed set E, bump functions for E inside shrinking neighbourhoods U_n converge pointwise to the indicator 1_E (isClosed_mem_L0). On a normal space, in particular a metric space, they exist by Urysohn's lemma (exists_isBumpFunction).

Implementation note: the predicate takes any sets E and U; closedness, openness and E ⊆ U are hypotheses of exists_isBumpFunction.

Blueprint: def:bump-function

• mem_Icc (x : X) : f x ∈ Set.Icc 0 1

  The function takes values in [0, 1].

• eq_one (x : X) : x ∈ E → f x = 1

  The function is 1 on E.

• support_subset : Function.support ⇑f ⊆ U

  The function is supported in U.

theorem Physicslib4.Spectral.exists_isBumpFunction {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {E U : Set X} (hE : IsClosed E) (hU : IsOpen U) (hEU : E ⊆ U) : ∃ (f : C(X, ℝ)), IsBumpFunction E U f

On a normal topological space, every closed set has a bump function supported in any given open neighbourhood of it.

Blueprint reference: thrm:existence-of-bump-functions.

The monotone class theorem

structure Physicslib4.Spectral.IsMonotoneClass {X : Type u_1} (ℳ : Set (Set X)) : Prop

A monotone class on X: a family of subsets closed under increasing unions and decreasing intersections of sequences.

If E_1 ⊆ E_2 ⊆ ⋯ all lie in the family, so does ⋃ E_n; if E_1 ⊇ E_2 ⊇ ⋯ all lie in it, so does ⋂ E_n. The monotone class theorem (generateFrom_subset_of_isMonotoneClass) says that a monotone class containing an algebra of sets contains the σ-algebra it generates; this is how a property of indicator functions is extended from open sets to all Borel sets.

Blueprint: the monotone classes of thrm:monotone-class-theorem

• iUnion_mem (f : ℕ → Set X) : Monotone f → (∀ (n : ℕ), f n ∈ ℳ) → ⋃ (n : ℕ), f n ∈ ℳ

  Closure under countable increasing unions.

• iInter_mem (f : ℕ → Set X) : Antitone f → (∀ (n : ℕ), f n ∈ ℳ) → ⋂ (n : ℕ), f n ∈ ℳ

  Closure under countable decreasing intersections.

theorem Physicslib4.Spectral.generateFrom_subset_of_isMonotoneClass {X : Type u_1} {𝒜 ℳ : Set (Set X)} (h𝒜 : MeasureTheory.IsSetAlgebra 𝒜) (hℳ : IsMonotoneClass ℳ) (h : 𝒜 ⊆ ℳ) : {s : Set X | MeasurableSet s} ⊆ ℳ

Monotone class theorem. A monotone class containing an algebra of sets contains the σ-algebra it generates.

Blueprint reference: thrm:monotone-class-theorem.

The class 𝓛₀

def Physicslib4.Spectral.L0 (X : Type u_1) [TopologicalSpace X] [MeasurableSpace X] : Set (Set X)

The class 𝓛₀ of sets E whose indicator 1_E is a pointwise limit of bounded continuous functions.

E ∈ 𝓛₀ when there are continuous f_n : X → ℝ and a constant C with |f_n(x)| ≤ C for all n and x, and f_n(x) → 1_E(x) for every x. The convergence is pointwise; uniform convergence would force 1_E to be continuous, so E clopen. On a metric space 𝓛₀ contains every closed set (isClosed_mem_L0) and is an algebra of sets containing the open sets (isSetAlgebra_L0); the monotone class theorem then takes the bootstrap from 𝓛₀ to all Borel sets.

Implementation note: the blueprint also asks that E be measurable. The definition omits this, since under the Borel σ-algebra every member is measurable (measurableSet_of_mem_L0); the extra conjunct would only add a derivable obligation to every membership proof.

Blueprint: def:L0-class

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.Spectral.empty_mem_L0 {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] : ∅ ∈ L0 X

The empty set lies in 𝓛₀, witnessed by the constant sequence 0.

Blueprint reference: prpstn:L0-contains-empty.

theorem Physicslib4.Spectral.compl_mem_L0 {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {E : Set X} (hE : E ∈ L0 X) : Eᶜ ∈ L0 X

𝓛₀ is closed under complements, witnessed by 1 - fₙ.

Blueprint reference: prpstn:L0-complement.

theorem Physicslib4.Spectral.union_mem_L0 {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {E F : Set X} (hE : E ∈ L0 X) (hF : F ∈ L0 X) : E ∪ F ∈ L0 X

𝓛₀ is closed under finite unions, witnessed by fₙ + gₙ - fₙ gₙ.

Blueprint reference: prpstn:L0-union.

theorem Physicslib4.Spectral.measurableSet_of_mem_L0 {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {E : Set X} (hE : E ∈ L0 X) : MeasurableSet E

A member of 𝓛₀ is measurable: its indicator is a pointwise limit of continuous, hence measurable, functions.

The bootstrap class 𝒞

The hypotheses on 𝒞 mention only bounded measurable functions, continuous real-valued functions and pointwise limits, so the definition is stated with no assumption on X beyond a topology and a σ-algebra. The metric Borel context (no compactness) is imposed on IsBorelGenerating.indicator_mem and IsBorelGenerating.eq_bddMeasurable below, which are the statements that really need it (through isClosed_mem_L0, hence through the bump functions).

structure Physicslib4.Spectral.IsBorelGenerating {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (𝒞 : Set (X → ℂ)) : Prop

A class 𝒞 of bounded measurable functions that is a subspace, contains the continuous real functions, and is closed under bounded pointwise limits.

These are the hypotheses of the bootstrap from continuous to bounded Borel functions. On a metric space with its Borel σ-algebra such a class contains the indicator of every Borel set (IsBorelGenerating.indicator_mem) and is in fact all bounded measurable functions (IsBorelGenerating.eq_bddMeasurable). This is how a property known for continuous f, such as multiplicativity of the functional calculus, is extended to every bounded Borel f: one shows that the functions with the property form such a class (isBorelGenerating_F1Class, isBorelGenerating_F2Class).

Implementation note: the structure assumes only a topology and a σ-algebra on X; the metric and Borel hypotheses are on the two theorems, which do not need compactness.

Blueprint: the hypotheses (1)–(3) of lmm:hall-prblm-8.3.3b

• bddMeasurable : 𝒞 ⊆ ↑(BddMeasurable X)

  Every member is bounded and measurable.

• smul_add_mem (α β : ℂ) (f g : X → ℂ) : f ∈ 𝒞 → g ∈ 𝒞 → α • f + β • g ∈ 𝒞

  𝒞 is a complex subspace.

• continuous_mem (f : C(X, ℝ)) : (fun (x : X) => ↑(f x)) ∈ 𝒞

  𝒞 contains the continuous real-valued functions.

• tendsto_mem (f : ℕ → X → ℂ) (g : X → ℂ) (M : ℝ) : (∀ (n : ℕ), f n ∈ 𝒞) → (BoundedPointwiseLimit f g fun (x : X) => M) → g ∈ 𝒞

  𝒞 is closed under uniformly bounded pointwise limits.

theorem Physicslib4.Spectral.isClosed_mem_L0 {X : Type u_1} [MetricSpace X] [MeasurableSpace X] {E : Set X} (hE : IsClosed E) : E ∈ L0 X

Every closed subset of X lies in 𝓛₀. This is the one closure property of 𝓛₀ that needs the metric (indeed, the bump functions of Physicslib4.Spectral.exists_isBumpFunction).

Blueprint reference: prpstn:L0-contains-closed.

theorem Physicslib4.Spectral.isSetAlgebra_L0 {X : Type u_1} [MetricSpace X] [MeasurableSpace X] : MeasureTheory.IsSetAlgebra (L0 X) ∧ ∀ (U : Set X), IsOpen U → U ∈ L0 X

𝓛₀ is an algebra of sets and contains every open subset of X.

This blueprint node is exactly the conjunction of empty_mem_L0, compl_mem_L0, union_mem_L0 and isClosed_mem_L0, so it is proved from them rather than restated.

Blueprint reference: lmm:hall-prblm-8.3.3a.

theorem Physicslib4.Spectral.IsBorelGenerating.indicator_mem {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {𝒞 : Set (X → ℂ)} (h𝒞 : IsBorelGenerating 𝒞) {E : Set X} (hE : MeasurableSet E) : E.indicator 1 ∈ 𝒞

The class 𝓛₁ of sets whose indicator lies in 𝒞 contains every Borel set.

Blueprint reference: lmm:hall-prblm-8.3.3b.

theorem Physicslib4.Spectral.IsBorelGenerating.eq_bddMeasurable {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {𝒞 : Set (X → ℂ)} (h𝒞 : IsBorelGenerating 𝒞) : 𝒞 = ↑(BddMeasurable X)

𝒞 is exactly the set of bounded Borel-measurable complex-valued functions on X.

Blueprint reference: lmm:hall-prblm-8.3.3c.