# Bounded continuous functions #

The type of bounded continuous functions taking values in a metric space, with the uniform distance.

`α →ᵇ β`

is the type of bounded continuous functions `α → β`

from a topological space to a
metric space.

When possible, instead of parametrizing results over `(f : α →ᵇ β)`

,
you should parametrize over `(F : Type*) [BoundedContinuousMapClass F α β] (f : F)`

.

When you extend this structure, make sure to extend `BoundedContinuousMapClass`

.

- toFun : α → β
- continuous_toFun : Continuous self.toFun

## Instances For

## Equations

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

## Instances For

`BoundedContinuousMapClass F α β`

states that `F`

is a type of bounded continuous maps.

You should also extend this typeclass when you extend `BoundedContinuousFunction`

.

- map_continuous : ∀ (f : F), Continuous ⇑f

## Instances

## Equations

- BoundedContinuousFunction.instFunLike = { coe := fun (f : BoundedContinuousFunction α β) => f.toFun, coe_injective' := ⋯ }

## Equations

- ⋯ = ⋯

## Equations

- BoundedContinuousFunction.instCoeTC = { coe := fun (f : F) => { toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ } }

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

## Equations

## Instances For

A continuous function with an explicit bound is a bounded continuous function.

## Equations

- BoundedContinuousFunction.mkOfBound f C h = { toContinuousMap := f, map_bounded' := ⋯ }

## Instances For

A continuous function on a compact space is automatically a bounded continuous function.

## Equations

- BoundedContinuousFunction.mkOfCompact f = { toContinuousMap := f, map_bounded' := ⋯ }

## Instances For

If a function is bounded on a discrete space, it is automatically continuous, and therefore gives rise to an element of the type of bounded continuous functions.

## Equations

- BoundedContinuousFunction.mkOfDiscrete f C h = { toFun := f, continuous_toFun := ⋯, map_bounded' := ⋯ }

## Instances For

The uniform distance between two bounded continuous functions.

The pointwise distance is controlled by the distance between functions, by definition.

The distance between two functions is controlled by the supremum of the pointwise distances.

The type of bounded continuous functions, with the uniform distance, is a pseudometric space.

## Equations

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

The type of bounded continuous functions, with the uniform distance, is a metric space.

## Equations

- BoundedContinuousFunction.instMetricSpace = MetricSpace.mk ⋯

On an empty space, bounded continuous functions are at distance 0.

The topology on `α →ᵇ β`

is exactly the topology induced by the natural map to `α →ᵤ β`

.

Constant as a continuous bounded function.

## Equations

- BoundedContinuousFunction.const α b = { toContinuousMap := ContinuousMap.const α b, map_bounded' := ⋯ }

## Instances For

If the target space is inhabited, so is the space of bounded continuous functions.

## Equations

- BoundedContinuousFunction.instInhabited = { default := BoundedContinuousFunction.const α default }

When `x`

is fixed, `(f : α →ᵇ β) ↦ f x`

is continuous.

The evaluation map is continuous, as a joint function of `u`

and `x`

.

Bounded continuous functions taking values in a complete space form a complete space.

## Equations

- ⋯ = ⋯

Composition of a bounded continuous function and a continuous function.

## Equations

- f.compContinuous g = { toContinuousMap := f.comp g, map_bounded' := ⋯ }

## Instances For

Restrict a bounded continuous function to a set.

## Equations

- f.restrict s = f.compContinuous (ContinuousMap.restrict s (ContinuousMap.id α))

## Instances For

Composition (in the target) of a bounded continuous function with a Lipschitz map again gives a bounded continuous function.

## Equations

- BoundedContinuousFunction.comp G H f = { toFun := fun (x : α) => G (f x), continuous_toFun := ⋯, map_bounded' := ⋯ }

## Instances For

The composition operator (in the target) with a Lipschitz map is Lipschitz.

The composition operator (in the target) with a Lipschitz map is uniformly continuous.

The composition operator (in the target) with a Lipschitz map is continuous.

Restriction (in the target) of a bounded continuous function taking values in a subset.

## Equations

- BoundedContinuousFunction.codRestrict s f H = { toFun := Set.codRestrict (⇑f) s H, continuous_toFun := ⋯, map_bounded' := ⋯ }

## Instances For

A version of `Function.extend`

for bounded continuous maps. We assume that the domain has
discrete topology, so we only need to verify boundedness.

## Equations

- BoundedContinuousFunction.extend f g h = { toFun := Function.extend ⇑f ⇑g ⇑h, continuous_toFun := ⋯, map_bounded' := ⋯ }

## Instances For

First version, with pointwise equicontinuity and range in a compact space.

Second version, with pointwise equicontinuity and range in a compact subset.

Third (main) version, with pointwise equicontinuity and range in a compact subset, but without closedness. The closure is then compact.

## Equations

- BoundedContinuousFunction.instZero = { zero := BoundedContinuousFunction.const α 0 }

## Equations

- BoundedContinuousFunction.instOne = { one := BoundedContinuousFunction.const α 1 }

The pointwise sum of two bounded continuous functions is again bounded continuous.

## Equations

- BoundedContinuousFunction.instAdd = { add := fun (f g : BoundedContinuousFunction α β) => { toFun := fun (x : α) => f x + g x, continuous_toFun := ⋯, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instSMulNat = { smul := fun (n : ℕ) (f : BoundedContinuousFunction α β) => { toContinuousMap := n • f.toContinuousMap, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instAddMonoid = Function.Injective.addMonoid (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯ ⋯ ⋯

Coercion of a `NormedAddGroupHom`

is an `AddMonoidHom`

. Similar to `AddMonoidHom.coeFn`

.

## Equations

- BoundedContinuousFunction.coeFnAddHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

## Instances For

The additive map forgetting that a bounded continuous function is bounded.

## Equations

- BoundedContinuousFunction.toContinuousMapAddHom α β = { toFun := BoundedContinuousFunction.toContinuousMap, map_zero' := ⋯, map_add' := ⋯ }

## Instances For

## Equations

- BoundedContinuousFunction.instAddAddCommMonoid = AddCommMonoid.mk ⋯

## Equations

- BoundedContinuousFunction.instAddCommMonoid = AddCommMonoid.mk ⋯

## Equations

- ⋯ = ⋯

The pointwise difference of two bounded continuous functions is again bounded continuous.

## Equations

- BoundedContinuousFunction.instSub = { sub := fun (f g : BoundedContinuousFunction α R) => { toFun := fun (x : α) => f x - g x, continuous_toFun := ⋯, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instNatCast = { natCast := fun (n : ℕ) => BoundedContinuousFunction.const α ↑n }

## Equations

- BoundedContinuousFunction.instIntCast = { intCast := fun (m : ℤ) => BoundedContinuousFunction.const α ↑m }

## Equations

- BoundedContinuousFunction.instMul = { mul := fun (f g : BoundedContinuousFunction α R) => { toFun := fun (x : α) => f x * g x, continuous_toFun := ⋯, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instPow = { pow := fun (f : BoundedContinuousFunction α R) (n : ℕ) => { toFun := fun (x : α) => f x ^ n, continuous_toFun := ⋯, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instMonoid = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

## Equations

- BoundedContinuousFunction.instCommMonoid = CommMonoid.mk ⋯

## Equations

- BoundedContinuousFunction.instSemiring = Function.Injective.semiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

## Equations

- BoundedContinuousFunction.instNorm = { norm := fun (x : BoundedContinuousFunction α β) => dist x 0 }

The norm of a bounded continuous function is the supremum of `‖f x‖`

.
We use `sInf`

to ensure that the definition works if `α`

has no elements.

When the domain is non-empty, we do not need the `0 ≤ C`

condition in the formula for `‖f‖`

as a
`sInf`

.

Distance between the images of any two points is at most twice the norm of the function.

The norm of a function is controlled by the supremum of the pointwise norms.

Norm of `const α b`

is less than or equal to `‖b‖`

. If `α`

is nonempty,
then it is equal to `‖b‖`

.

Constructing a bounded continuous function from a uniformly bounded continuous function taking values in a normed group.

## Equations

- BoundedContinuousFunction.ofNormedAddCommGroup f Hf C H = { toFun := fun (n : α) => f n, continuous_toFun := Hf, map_bounded' := ⋯ }

## Instances For

Constructing a bounded continuous function from a uniformly bounded function on a discrete space, taking values in a normed group.

## Equations

## Instances For

Taking the pointwise norm of a bounded continuous function with values in a
`SeminormedAddCommGroup`

yields a bounded continuous function with values in ℝ.

## Equations

- f.normComp = BoundedContinuousFunction.comp norm ⋯ f

## Instances For

If `‖(1 : β)‖ = 1`

, then `‖(1 : α →ᵇ β)‖ = 1`

if `α`

is nonempty.

## Equations

- ⋯ = ⋯

The pointwise opposite of a bounded continuous function is again bounded continuous.

## Equations

- BoundedContinuousFunction.instNeg = { neg := fun (f : BoundedContinuousFunction α β) => BoundedContinuousFunction.ofNormedAddCommGroup (-⇑f) ⋯ ‖f‖ ⋯ }

## Equations

- BoundedContinuousFunction.instSMulInt = { smul := fun (n : ℤ) (f : BoundedContinuousFunction α β) => { toContinuousMap := n • f.toContinuousMap, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instAddCommGroup = Function.Injective.addCommGroup (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

## Equations

- BoundedContinuousFunction.instSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

## Equations

- BoundedContinuousFunction.instNormedAddCommGroup = NormedAddCommGroup.mk ⋯

The `nnnorm`

of a function is controlled by the supremum of the pointwise `nnnorm`

s.

`BoundedSMul`

(in particular, topological module) structure #

In this section, if `β`

is a metric space and a `𝕜`

-module whose addition and scalar multiplication
are compatible with the metric structure, then we show that the space of bounded continuous
functions from `α`

to `β`

inherits a so-called `BoundedSMul`

structure (in particular, a
`ContinuousMul`

structure, which is the mathlib formulation of being a topological module), by
using pointwise operations and checking that they are compatible with the uniform distance.

## Equations

- BoundedContinuousFunction.instSMul = { smul := fun (c : 𝕜) (f : BoundedContinuousFunction α β) => { toContinuousMap := c • f.toContinuousMap, map_bounded' := ⋯ } }

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- BoundedContinuousFunction.instMulAction = Function.Injective.mulAction (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯

## Equations

- BoundedContinuousFunction.instDistribMulAction = Function.Injective.distribMulAction { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

## Equations

- BoundedContinuousFunction.instModule = Function.Injective.module 𝕜 { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

The evaluation at a point, as a continuous linear map from `α →ᵇ β`

to `β`

.

## Equations

- BoundedContinuousFunction.evalCLM 𝕜 x = { toFun := fun (f : BoundedContinuousFunction α β) => f x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

## Instances For

The linear map forgetting that a bounded continuous function is bounded.

## Equations

- BoundedContinuousFunction.toContinuousMapLinearMap α β 𝕜 = { toFun := BoundedContinuousFunction.toContinuousMap, map_add' := ⋯, map_smul' := ⋯ }

## Instances For

### Normed space structure #

In this section, if `β`

is a normed space, then we show that the space of bounded
continuous functions from `α`

to `β`

inherits a normed space structure, by using
pointwise operations and checking that they are compatible with the uniform distance.

## Equations

- BoundedContinuousFunction.instNormedSpace = NormedSpace.mk ⋯

Postcomposition of bounded continuous functions into a normed module by a continuous linear map
is a continuous linear map.
Upgraded version of `ContinuousLinearMap.compLeftContinuous`

, similar to `LinearMap.compLeft`

.

## Equations

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

## Instances For

### Normed ring structure #

In this section, if `R`

is a normed ring, then we show that the space of bounded
continuous functions from `α`

to `R`

inherits a normed ring structure, by using
pointwise operations and checking that they are compatible with the uniform distance.

## Equations

- BoundedContinuousFunction.instNonUnitalRing = Function.Injective.nonUnitalRing (fun (f : BoundedContinuousFunction α R) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

## Equations

- BoundedContinuousFunction.instNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

## Equations

- BoundedContinuousFunction.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

## Equations

- BoundedContinuousFunction.hasNatPow = { pow := fun (f : BoundedContinuousFunction α R) (n : ℕ) => { toContinuousMap := f.toContinuousMap ^ n, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instNatCast_1 = { natCast := fun (n : ℕ) => BoundedContinuousFunction.const α ↑n }

## Equations

- BoundedContinuousFunction.instIntCast_1 = { intCast := fun (n : ℤ) => BoundedContinuousFunction.const α ↑n }

## Equations

- BoundedContinuousFunction.instRing = Function.Injective.ring (fun (f : BoundedContinuousFunction α R) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

## Equations

- BoundedContinuousFunction.instSeminormedRing = SeminormedRing.mk ⋯ ⋯

## Equations

- BoundedContinuousFunction.instNormedRing = NormedRing.mk ⋯ ⋯

### Normed commutative ring structure #

In this section, if `R`

is a normed commutative ring, then we show that the space of bounded
continuous functions from `α`

to `R`

inherits a normed commutative ring structure, by using
pointwise operations and checking that they are compatible with the uniform distance.

## Equations

- BoundedContinuousFunction.instCommRing = CommRing.mk ⋯

## Equations

- BoundedContinuousFunction.instSeminormedCommRing = SeminormedCommRing.mk ⋯

## Equations

- BoundedContinuousFunction.instNormedCommRing = NormedCommRing.mk ⋯

### Normed algebra structure #

In this section, if `γ`

is a normed algebra, then we show that the space of bounded
continuous functions from `α`

to `γ`

inherits a normed algebra structure, by using
pointwise operations and checking that they are compatible with the uniform distance.

`BoundedContinuousFunction.const`

as a `RingHom`

.

## Equations

- BoundedContinuousFunction.C = { toFun := fun (c : 𝕜) => BoundedContinuousFunction.const α ((algebraMap 𝕜 γ) c), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

## Instances For

## Equations

- BoundedContinuousFunction.instAlgebra = Algebra.mk BoundedContinuousFunction.C ⋯ ⋯

## Equations

- BoundedContinuousFunction.instNormedAlgebra = NormedAlgebra.mk ⋯

### Structure as normed module over scalar functions #

If `β`

is a normed `𝕜`

-space, then we show that the space of bounded continuous
functions from `α`

to `β`

is naturally a module over the algebra of bounded continuous
functions from `α`

to `𝕜`

.

## Equations

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

## Equations

- BoundedContinuousFunction.instModule' = Module.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯

## Equations

- ⋯ = ⋯

### Star structures #

In this section, if `β`

is a normed ⋆-group, then so is the space of bounded
continuous functions from `α`

to `β`

, by using the star operation pointwise.

If `𝕜`

is normed field and a ⋆-ring over which `β`

is a normed algebra and a
star module, then the space of bounded continuous functions from `α`

to `β`

is a star module.

If `β`

is a ⋆-ring in addition to being a normed ⋆-group, then `α →ᵇ β`

inherits a ⋆-ring structure.

In summary, if `β`

is a C⋆-algebra over `𝕜`

, then so is `α →ᵇ β`

; note that
completeness is guaranteed when `β`

is complete (see
`BoundedContinuousFunction.complete`

).

## Equations

- BoundedContinuousFunction.instStarAddMonoid = StarAddMonoid.mk ⋯

The right-hand side of this equality can be parsed `star ∘ ⇑f`

because of the
instance `Pi.instStarForAll`

. Upon inspecting the goal, one sees `⊢ ↑(star f) = star ↑f`

.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- BoundedContinuousFunction.instStarRing = StarRing.mk ⋯

## Equations

- ⋯ = ⋯

## Equations

- BoundedContinuousFunction.instPartialOrder = PartialOrder.lift (fun (f : BoundedContinuousFunction α β) => f.toFun) ⋯

## Equations

- BoundedContinuousFunction.instSup = { sup := fun (f g : BoundedContinuousFunction α β) => { toFun := ⇑f ⊔ ⇑g, continuous_toFun := ⋯, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instInf = { inf := fun (f g : BoundedContinuousFunction α β) => { toFun := ⇑f ⊓ ⇑g, continuous_toFun := ⋯, map_bounded' := ⋯ } }

## Equations

- BoundedContinuousFunction.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯

## Equations

- BoundedContinuousFunction.instSemilatticeInf = Function.Injective.semilatticeInf (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯

## Equations

- BoundedContinuousFunction.instLattice = Function.Injective.lattice (fun (f : BoundedContinuousFunction α β) => ⇑f) ⋯ ⋯ ⋯

**Alias** of `BoundedContinuousFunction.coe_sup`

.

**Alias** of `BoundedContinuousFunction.coe_abs`

.

## Equations

- BoundedContinuousFunction.instNormedLatticeAddCommGroup = NormedLatticeAddCommGroup.mk ⋯

The nonnegative part of a bounded continuous `ℝ`

-valued function as a bounded
continuous `ℝ≥0`

-valued function.

## Equations

## Instances For

The absolute value of a bounded continuous `ℝ`

-valued function as a bounded
continuous `ℝ≥0`

-valued function.

## Equations

- f.nnnorm = BoundedContinuousFunction.comp (fun (x : ℝ) => ‖x‖₊) BoundedContinuousFunction.nnnorm.proof_1 f

## Instances For

Decompose a bounded continuous function to its positive and negative parts.

Express the absolute value of a bounded continuous function in terms of its positive and negative parts.