Bounded Borel symbols

Bounded measurable complex functions form a commutative C⋆-algebra under pointwise operations and the supremum norm. They are realised as the star subalgebra of ℓ^∞(X, ℂ), Mathlib's lp (fun _ : X ↦ ℂ) ∞, cut out by measurability, so the supremum norm, the normed star algebra structure and the C⋆-identity are those of ℓ^∞. Uniform limits of measurable functions are measurable, so this subalgebra is closed and the symbols form a complete space.

Equality is pointwise; no measure or almost-everywhere quotient is involved. On a topological space equipped with its Borel measurable space these are bounded Borel functions. The domain may be empty, in which case every norm vanishes; on a nonempty domain the unit has norm one.

These symbols form the source algebra for bounded Borel functional calculus: constants, measurable simple functions and restrictions to measurable sets are bounded symbols, pullback along a measurable map is a star algebra homomorphism (hence norm-nonincreasing, as is every star homomorphism between C⋆-algebras), and convergence in norm is uniform convergence.

Simple functions embed as a star subalgebra of symbols, and this subalgebra is dense: every symbol is the uniform limit of simple symbols bounded by its norm (exists_seq_tendsto_ofSimpleFunc). Since a simple symbol is a finite combination of indicators of disjoint measurable sets, this is the approximation through which a functional calculus defined on indicators extends by continuity to all bounded Borel symbols.

On a compact space whose open sets are measurable, continuous complex functions are bounded Borel symbols (ofContinuousMap). This embedding of C(X, ℂ) is a unital star algebra homomorphism, is isometric for the two supremum norms, and is compatible with pullback along continuous measurable maps. It is how a Borel functional calculus is compared with a continuous one, for instance with a star representation of C(X, ℂ) or with Mathlib's continuous functional calculus cfcHom.

def TauCeti.boundedBorelSubalgebra (X : Type u_1) [MeasurableSpace X] : StarSubalgebra ℂ ↥(lp (fun (x : X) => ℂ) ⊤)

The star subalgebra of ℓ^∞(X, ℂ) consisting of the measurable bounded functions.

@[simp]

theorem TauCeti.mem_boundedBorelSubalgebra (X : Type u_1) [MeasurableSpace X] (f : ↥(lp (fun (x : X) => ℂ) ⊤)) : f ∈ boundedBorelSubalgebra X ↔ Measurable ↑f

An element of ℓ^∞(X, ℂ) is a bounded Borel symbol exactly when it is measurable.

theorem TauCeti.isClosed_boundedBorelSubalgebra (X : Type u_1) [MeasurableSpace X] : IsClosed ↑(boundedBorelSubalgebra X)

Uniform limits of measurable functions are measurable, so the bounded Borel symbols form a closed subalgebra of ℓ^∞(X, ℂ).

@[reducible, inline]

abbrev TauCeti.BoundedBorelFunction (X : Type u_1) [MeasurableSpace X] : Type u_1

Bounded Borel symbols, with the pointwise algebra and the supremum norm of ℓ^∞.

instance TauCeti.BoundedBorelFunction.instCompleteSpace (X : Type u_1) [MeasurableSpace X] : CompleteSpace (BoundedBorelFunction X)

Bounded Borel symbols form a Banach space, since they form a closed subspace of ℓ^∞.

@[instance_reducible]

noncomputable instance TauCeti.BoundedBorelFunction.instCommCStarAlgebra (X : Type u_1) [MeasurableSpace X] : CommCStarAlgebra (BoundedBorelFunction X)

Bounded Borel symbols form a commutative unital C⋆-algebra, as a closed star subalgebra of ℓ^∞(X, ℂ).

@[instance_reducible]

instance TauCeti.BoundedBorelFunction.instFunLikeComplex {X : Type u_1} [MeasurableSpace X] : FunLike (BoundedBorelFunction X) X ℂ

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_val {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : ↑↑f = ⇑f

Evaluating the underlying element of ℓ^∞ is evaluating the symbol.

theorem TauCeti.BoundedBorelFunction.coe_injective {X : Type u_1} [MeasurableSpace X] : Function.Injective DFunLike.coe

Function coercion determines a bounded Borel symbol.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_zero {X : Type u_1} [MeasurableSpace X] : ⇑0 = 0

The zero symbol coerces to the zero function.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_one {X : Type u_1} [MeasurableSpace X] : ⇑1 = 1

The unit symbol coerces to the constant unit function.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_add {X : Type u_1} [MeasurableSpace X] (f g : BoundedBorelFunction X) : ⇑(f + g) = ⇑f + ⇑g

Function coercion preserves addition.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_neg {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : ⇑(-f) = -⇑f

Function coercion preserves negation.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_sub {X : Type u_1} [MeasurableSpace X] (f g : BoundedBorelFunction X) : ⇑(f - g) = ⇑f - ⇑g

Function coercion preserves subtraction.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_mul {X : Type u_1} [MeasurableSpace X] (f g : BoundedBorelFunction X) : ⇑(f * g) = ⇑f * ⇑g

Function coercion preserves multiplication.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_smul {X : Type u_1} [MeasurableSpace X] (c : ℂ) (f : BoundedBorelFunction X) : ⇑(c • f) = c • ⇑f

Function coercion preserves scalar multiplication.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_star {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : ⇑(star f) = star ⇑f

Function coercion preserves the star operation.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_pow {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) (n : ℕ) : ⇑(f ^ n) = ⇑f ^ n

Function coercion preserves natural powers.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_algebraMap {X : Type u_1} [MeasurableSpace X] (c : ℂ) : ⇑((algebraMap ℂ (BoundedBorelFunction X)) c) = fun (x : X) => c

Algebra scalars coerce to constant functions.

theorem TauCeti.BoundedBorelFunction.ext {X : Type u_1} [MeasurableSpace X] {f g : BoundedBorelFunction X} (h : ∀ (x : X), f x = g x) : f = g

Two symbols are equal when they agree at every point.

theorem TauCeti.BoundedBorelFunction.ext_iff {X : Type u_1} [MeasurableSpace X] {f g : BoundedBorelFunction X} : f = g ↔ ∀ (x : X), f x = g x

theorem TauCeti.BoundedBorelFunction.measurable {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : Measurable ⇑f

Evaluation of a bounded Borel symbol is measurable.

theorem TauCeti.BoundedBorelFunction.norm_eq_iSup_norm {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : ‖f‖ = ⨆ (x : X), ‖f x‖

The norm of a symbol is the supremum of the norms of its values.

theorem TauCeti.BoundedBorelFunction.norm_coe_le_norm {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) (x : X) : ‖f x‖ ≤ ‖f‖

Each value of a symbol is bounded in norm by the supremum norm.

theorem TauCeti.BoundedBorelFunction.norm_le {X : Type u_1} [MeasurableSpace X] {f : BoundedBorelFunction X} {C : ℝ} (hC : 0 ≤ C) : ‖f‖ ≤ C ↔ ∀ (x : X), ‖f x‖ ≤ C

A nonnegative constant bounds the supremum norm exactly when it bounds every value.

theorem TauCeti.BoundedBorelFunction.norm_eq_zero_of_empty {X : Type u_1} [MeasurableSpace X] [IsEmpty X] (f : BoundedBorelFunction X) : ‖f‖ = 0

On an empty domain every symbol has norm zero.

theorem TauCeti.BoundedBorelFunction.tendsto_iff_tendstoUniformly {X : Type u_1} [MeasurableSpace X] {ι : Type u_2} {F : ι → BoundedBorelFunction X} {f : BoundedBorelFunction X} {l : Filter ι} : Filter.Tendsto F l (nhds f) ↔ TendstoUniformly (fun (i : ι) => ⇑(F i)) (⇑f) l

Convergence in the supremum norm is uniform convergence of the values.

theorem TauCeti.BoundedBorelFunction.exists_bound {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : X), ‖f x‖ ≤ M

Every symbol has a nonnegative bound valid at every point, including on an empty domain.

theorem TauCeti.BoundedBorelFunction.integrable {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (⇑f) μ

A symbol is integrable against every finite measure.

def TauCeti.BoundedBorelFunction.ofFunction {X : Type u_1} [MeasurableSpace X] (f : X → ℂ) (hf : Measurable f) (hbound : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : X), ‖f x‖ ≤ M) : BoundedBorelFunction X

Bundle a measurable function with its everywhere bound.

@[simp]

theorem TauCeti.BoundedBorelFunction.ofFunction_apply {X : Type u_1} [MeasurableSpace X] (f : X → ℂ) (hf : Measurable f) (hbound : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : X), ‖f x‖ ≤ M) (x : X) : (ofFunction f hf hbound) x = f x

Bundling preserves evaluation.

@[simp]

theorem TauCeti.BoundedBorelFunction.algebraMap_apply {X : Type u_1} [MeasurableSpace X] (c : ℂ) (x : X) : ((algebraMap ℂ (BoundedBorelFunction X)) c) x = c

Evaluation of an algebra scalar is the constant scalar.

@[simp]

theorem TauCeti.BoundedBorelFunction.zero_apply {X : Type u_1} [MeasurableSpace X] (x : X) : 0 x = 0

Evaluation of zero.

@[simp]

theorem TauCeti.BoundedBorelFunction.one_apply {X : Type u_1} [MeasurableSpace X] (x : X) : 1 x = 1

Evaluation of one.

@[simp]

theorem TauCeti.BoundedBorelFunction.add_apply {X : Type u_1} [MeasurableSpace X] (f g : BoundedBorelFunction X) (x : X) : (f + g) x = f x + g x

Evaluation of addition.

@[simp]

theorem TauCeti.BoundedBorelFunction.neg_apply {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) (x : X) : (-f) x = -f x

Evaluation of negation.

@[simp]

theorem TauCeti.BoundedBorelFunction.sub_apply {X : Type u_1} [MeasurableSpace X] (f g : BoundedBorelFunction X) (x : X) : (f - g) x = f x - g x

Evaluation of subtraction.

@[simp]

theorem TauCeti.BoundedBorelFunction.mul_apply {X : Type u_1} [MeasurableSpace X] (f g : BoundedBorelFunction X) (x : X) : (f * g) x = f x * g x

Evaluation of multiplication.

@[simp]

theorem TauCeti.BoundedBorelFunction.smul_apply {X : Type u_1} [MeasurableSpace X] (c : ℂ) (f : BoundedBorelFunction X) (x : X) : (c • f) x = c * f x

Evaluation of scalar multiplication.

@[simp]

theorem TauCeti.BoundedBorelFunction.star_apply {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) (x : X) : (star f) x = star (f x)

Evaluation of the star operation is complex conjugation.

def TauCeti.BoundedBorelFunction.compStarAlgHom' {X : Type u_1} [MeasurableSpace X] {Y : Type u_2} [MeasurableSpace Y] (g : X → Y) (hg : Measurable g) : BoundedBorelFunction Y →⋆ₐ[ℂ] BoundedBorelFunction X

Pullback of symbols along a measurable map, as a star algebra homomorphism.

@[simp]

theorem TauCeti.BoundedBorelFunction.compStarAlgHom'_apply {X : Type u_1} [MeasurableSpace X] {Y : Type u_2} [MeasurableSpace Y] (g : X → Y) (hg : Measurable g) (f : BoundedBorelFunction Y) (x : X) : ((compStarAlgHom' g hg) f) x = f (g x)

Pullback evaluates by composition.

@[simp]

theorem TauCeti.BoundedBorelFunction.compStarAlgHom'_id {X : Type u_1} [MeasurableSpace X] : compStarAlgHom' id ⋯ = StarAlgHom.id ℂ (BoundedBorelFunction X)

Pullback by the identity is the identity star algebra homomorphism.

theorem TauCeti.BoundedBorelFunction.compStarAlgHom'_comp {X : Type u_1} [MeasurableSpace X] {Y : Type u_2} {Z : Type u_3} [MeasurableSpace Y] [MeasurableSpace Z] (g : X → Y) (hg : Measurable g) (h : Y → Z) (hh : Measurable h) : compStarAlgHom' (h ∘ g) ⋯ = (compStarAlgHom' g hg).comp (compStarAlgHom' h hh)

Pullback along a composite is composition of the star algebra homomorphisms.

noncomputable def TauCeti.BoundedBorelFunction.indicator {X : Type u_1} [MeasurableSpace X] (s : Set X) (hs : MeasurableSet s) : BoundedBorelFunction X →⋆ₙₐ[ℂ] BoundedBorelFunction X

Restriction to a measurable set and extension by zero, as a non-unital star algebra homomorphism. It need not preserve the unit because the unit restricts to the set indicator.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_indicator {X : Type u_1} [MeasurableSpace X] (s : Set X) (hs : MeasurableSet s) (f : BoundedBorelFunction X) : ⇑((indicator s hs) f) = s.indicator ⇑f

Restriction coerces to the usual set indicator function.

@[simp]

theorem TauCeti.BoundedBorelFunction.indicator_apply {X : Type u_1} [MeasurableSpace X] (s : Set X) (hs : MeasurableSet s) (f : BoundedBorelFunction X) (x : X) : ((indicator s hs) f) x = s.indicator (⇑f) x

Indicator evaluation is the usual set indicator.

@[simp]

theorem TauCeti.BoundedBorelFunction.indicator_empty {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : (indicator ∅ ⋯) f = 0

The indicator of the empty set vanishes.

@[simp]

theorem TauCeti.BoundedBorelFunction.indicator_univ {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : (indicator Set.univ ⋯) f = f

The indicator of the whole domain is the original symbol.

theorem TauCeti.BoundedBorelFunction.indicator_mul_indicator {X : Type u_1} [MeasurableSpace X] (s t : Set X) (hs : MeasurableSet s) (ht : MeasurableSet t) (f g : BoundedBorelFunction X) : (indicator s hs) f * (indicator t ht) g = (indicator (s ∩ t) ⋯) (f * g)

Products of indicator symbols correspond to intersections.

theorem TauCeti.BoundedBorelFunction.compStarAlgHom'_indicator {X : Type u_1} [MeasurableSpace X] {Y : Type u_2} [MeasurableSpace Y] (g : X → Y) (hg : Measurable g) (s : Set Y) (hs : MeasurableSet s) (f : BoundedBorelFunction Y) : (compStarAlgHom' g hg) ((indicator s hs) f) = (indicator (g ⁻¹' s) ⋯) ((compStarAlgHom' g hg) f)

Pullback commutes with restriction and extension by zero.

noncomputable def TauCeti.BoundedBorelFunction.ofSimpleFunc {X : Type u_1} [MeasurableSpace X] : MeasureTheory.SimpleFunc X ℂ →⋆ₐ[ℂ] BoundedBorelFunction X

Every measurable complex simple function is an everywhere bounded symbol. This embedding is a star algebra homomorphism for the pointwise operations on simple functions.

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_ofSimpleFunc {X : Type u_1} [MeasurableSpace X] (f : MeasureTheory.SimpleFunc X ℂ) : ⇑(ofSimpleFunc f) = ⇑f

A bundled simple function coerces to the simple function itself.

@[simp]

theorem TauCeti.BoundedBorelFunction.ofSimpleFunc_apply {X : Type u_1} [MeasurableSpace X] (f : MeasureTheory.SimpleFunc X ℂ) (x : X) : (ofSimpleFunc f) x = f x

Bundling a simple function preserves its values.

theorem TauCeti.BoundedBorelFunction.ofSimpleFunc_piecewise_const_zero {X : Type u_1} [MeasurableSpace X] (s : Set X) (hs : MeasurableSet s) (c : ℂ) : ofSimpleFunc (MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const X c) 0) = c • (indicator s hs) 1

The simple function equal to c on a measurable set s and to zero off s is the symbol c • indicator s hs 1.

theorem TauCeti.BoundedBorelFunction.exists_seq_tendsto_ofSimpleFunc {X : Type u_1} [MeasurableSpace X] (f : BoundedBorelFunction X) : ∃ (g : ℕ → MeasureTheory.SimpleFunc X ℂ), (∀ (n : ℕ) (x : X), ‖(g n) x‖ ≤ ‖f‖) ∧ Filter.Tendsto (fun (n : ℕ) => ofSimpleFunc (g n)) Filter.atTop (nhds f)

Uniform approximation by simple symbols. Every bounded Borel symbol is the limit, in the supremum norm, of simple symbols whose values are bounded by its norm.

theorem TauCeti.BoundedBorelFunction.denseRange_ofSimpleFunc {X : Type u_1} [MeasurableSpace X] : DenseRange ⇑ofSimpleFunc

Simple symbols are dense among bounded Borel symbols.

noncomputable def TauCeti.BoundedBorelFunction.ofContinuousMap {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [CompactSpace X] : C(X, ℂ) →⋆ₐ[ℂ] BoundedBorelFunction X

On a compact space whose open sets are measurable, every continuous complex function is a bounded Borel symbol. This embedding is a unital star algebra homomorphism for the pointwise operations on C(X, ℂ), and it is isometric for the supremum norms (norm_ofContinuousMap).

@[simp]

theorem TauCeti.BoundedBorelFunction.coe_ofContinuousMap {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [CompactSpace X] (f : C(X, ℂ)) : ⇑(ofContinuousMap f) = ⇑f

A continuous function regarded as a symbol coerces to the function itself.

@[simp]

theorem TauCeti.BoundedBorelFunction.ofContinuousMap_apply {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [CompactSpace X] (f : C(X, ℂ)) (x : X) : (ofContinuousMap f) x = f x

Regarding a continuous function as a symbol preserves its values.

theorem TauCeti.BoundedBorelFunction.norm_ofContinuousMap {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [CompactSpace X] (f : C(X, ℂ)) : ‖ofContinuousMap f‖ = ‖f‖

The supremum norm of a continuous function regarded as a symbol is its supremum norm as a continuous function.

theorem TauCeti.BoundedBorelFunction.isometry_ofContinuousMap {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [CompactSpace X] : Isometry ⇑ofContinuousMap

Regarding continuous functions as symbols is an isometry.

@[simp]

theorem TauCeti.BoundedBorelFunction.compStarAlgHom'_ofContinuousMap {X : Type u_1} [MeasurableSpace X] {Y : Type u_2} [MeasurableSpace Y] [TopologicalSpace X] [OpensMeasurableSpace X] [CompactSpace X] [TopologicalSpace Y] [OpensMeasurableSpace Y] [CompactSpace Y] (φ : C(X, Y)) (hφ : Measurable ⇑φ) (g : C(Y, ℂ)) : (compStarAlgHom' (⇑φ) hφ) (ofContinuousMap g) = ofContinuousMap (g.comp φ)

Pulling back a continuous function along a continuous measurable map between compact spaces gives the symbol of the composite continuous function.