# Bounded continuous functions #

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

structure BoundedContinuousFunction (α : Type u) (β : Type v) [] extends :
Type (max u v)

α →ᵇ β 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
• map_bounded' : ∃ (C : ), ∀ (x y : α), dist (self.toFun x) (self.toFun y) C
Instances For
theorem BoundedContinuousFunction.map_bounded' {α : Type u} {β : Type v} [] (self : ) :
∃ (C : ), ∀ (x y : α), dist (self.toFun x) (self.toFun y) C
Equations
• One or more equations did not get rendered due to their size.
Instances For
class BoundedContinuousMapClass (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [] [FunLike F α β] extends :

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),
• map_bounded : ∀ (f : F), ∃ (C : ), ∀ (x y : α), dist (f x) (f y) C
Instances
theorem BoundedContinuousMapClass.map_bounded {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [] [FunLike F α β] [self : ] (f : F) :
∃ (C : ), ∀ (x y : α), dist (f x) (f y) C
instance BoundedContinuousFunction.instFunLike {α : Type u} {β : Type v} [] :
FunLike α β
Equations
• BoundedContinuousFunction.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
Equations
• =
instance BoundedContinuousFunction.instCoeTC {F : Type u_1} {α : Type u} {β : Type v} [] [FunLike F α β] [] :
Equations
• BoundedContinuousFunction.instCoeTC = { coe := fun (f : F) => { toFun := f, continuous_toFun := , map_bounded' := } }
@[simp]
theorem BoundedContinuousFunction.coe_to_continuous_fun {α : Type u} {β : Type v} [] (f : ) :
f.toContinuousMap = f
def BoundedContinuousFunction.Simps.apply {α : Type u} {β : Type v} [] (h : ) :
αβ

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
theorem BoundedContinuousFunction.bounded {α : Type u} {β : Type v} [] (f : ) :
∃ (C : ), ∀ (x y : α), dist (f x) (f y) C
theorem BoundedContinuousFunction.continuous {α : Type u} {β : Type v} [] (f : ) :
theorem BoundedContinuousFunction.ext {α : Type u} {β : Type v} [] {f : } {g : } (h : ∀ (x : α), f x = g x) :
f = g
theorem BoundedContinuousFunction.isBounded_range {α : Type u} {β : Type v} [] (f : ) :
theorem BoundedContinuousFunction.isBounded_image {α : Type u} {β : Type v} [] (f : ) (s : Set α) :
theorem BoundedContinuousFunction.eq_of_empty {α : Type u} {β : Type v} [] [h : ] (f : ) (g : ) :
f = g
def BoundedContinuousFunction.mkOfBound {α : Type u} {β : Type v} [] (f : C(α, β)) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :

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

Equations
• = { toContinuousMap := f, map_bounded' := }
Instances For
@[simp]
theorem BoundedContinuousFunction.mkOfBound_coe {α : Type u} {β : Type v} [] {f : C(α, β)} {C : } {h : ∀ (x y : α), dist (f x) (f y) C} :
= f
def BoundedContinuousFunction.mkOfCompact {α : Type u} {β : Type v} [] [] (f : C(α, β)) :

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

Equations
• = { toContinuousMap := f, map_bounded' := }
Instances For
@[simp]
theorem BoundedContinuousFunction.mkOfCompact_apply {α : Type u} {β : Type v} [] [] (f : C(α, β)) (a : α) :
@[simp]
theorem BoundedContinuousFunction.mkOfDiscrete_toFun {α : Type u} {β : Type v} [] [] (f : αβ) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :
∀ (a : α), = f a
@[simp]
theorem BoundedContinuousFunction.mkOfDiscrete_apply {α : Type u} {β : Type v} [] [] (f : αβ) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :
∀ (a : α), = f a
def BoundedContinuousFunction.mkOfDiscrete {α : Type u} {β : Type v} [] [] (f : αβ) (C : ) (h : ∀ (x y : α), dist (f x) (f y) C) :

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
• = { toFun := f, continuous_toFun := , map_bounded' := }
Instances For
instance BoundedContinuousFunction.instDist {α : Type u} {β : Type v} [] :

The uniform distance between two bounded continuous functions.

Equations
• BoundedContinuousFunction.instDist = { dist := fun (f g : ) => sInf {C : | 0 C ∀ (x : α), dist (f x) (g x) C} }
theorem BoundedContinuousFunction.dist_eq {α : Type u} {β : Type v} [] {f : } {g : } :
dist f g = sInf {C : | 0 C ∀ (x : α), dist (f x) (g x) C}
theorem BoundedContinuousFunction.dist_set_exists {α : Type u} {β : Type v} [] {f : } {g : } :
∃ (C : ), 0 C ∀ (x : α), dist (f x) (g x) C
theorem BoundedContinuousFunction.dist_coe_le_dist {α : Type u} {β : Type v} [] {f : } {g : } (x : α) :
dist (f x) (g x) dist f g

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

theorem BoundedContinuousFunction.dist_le {α : Type u} {β : Type v} [] {f : } {g : } {C : } (C0 : 0 C) :
dist f g C ∀ (x : α), dist (f x) (g x) C

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

theorem BoundedContinuousFunction.dist_le_iff_of_nonempty {α : Type u} {β : Type v} [] {f : } {g : } {C : } [] :
dist f g C ∀ (x : α), dist (f x) (g x) C
theorem BoundedContinuousFunction.dist_lt_of_nonempty_compact {α : Type u} {β : Type v} [] {f : } {g : } {C : } [] [] (w : ∀ (x : α), dist (f x) (g x) < C) :
dist f g < C
theorem BoundedContinuousFunction.dist_lt_iff_of_compact {α : Type u} {β : Type v} [] {f : } {g : } {C : } [] (C0 : 0 < C) :
dist f g < C ∀ (x : α), dist (f x) (g x) < C
theorem BoundedContinuousFunction.dist_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [] {f : } {g : } {C : } [] [] :
dist f g < C ∀ (x : α), dist (f x) (g x) < C

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.
instance BoundedContinuousFunction.instMetricSpace {α : Type u} [] {β : Type u_2} [] :

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

Equations
• BoundedContinuousFunction.instMetricSpace =
theorem BoundedContinuousFunction.nndist_eq {α : Type u} {β : Type v} [] {f : } {g : } :
nndist f g = sInf {C : NNReal | ∀ (x : α), nndist (f x) (g x) C}
theorem BoundedContinuousFunction.nndist_set_exists {α : Type u} {β : Type v} [] {f : } {g : } :
∃ (C : NNReal), ∀ (x : α), nndist (f x) (g x) C
theorem BoundedContinuousFunction.nndist_coe_le_nndist {α : Type u} {β : Type v} [] {f : } {g : } (x : α) :
nndist (f x) (g x) nndist f g
theorem BoundedContinuousFunction.dist_zero_of_empty {α : Type u} {β : Type v} [] {f : } {g : } [] :
dist f g = 0

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

theorem BoundedContinuousFunction.dist_eq_iSup {α : Type u} {β : Type v} [] {f : } {g : } :
dist f g = ⨆ (x : α), dist (f x) (g x)
theorem BoundedContinuousFunction.nndist_eq_iSup {α : Type u} {β : Type v} [] {f : } {g : } :
nndist f g = ⨆ (x : α), nndist (f x) (g x)
theorem BoundedContinuousFunction.tendsto_iff_tendstoUniformly {α : Type u} {β : Type v} [] {ι : Type u_2} {F : } {f : } {l : } :
Filter.Tendsto F l (nhds f) TendstoUniformly (fun (i : ι) => (F i)) (f) l
theorem BoundedContinuousFunction.inducing_coeFn {α : Type u} {β : Type v} [] :
Inducing (UniformFun.ofFun DFunLike.coe)

The topology on α →ᵇ β is exactly the topology induced by the natural map to α →ᵤ β.

theorem BoundedContinuousFunction.embedding_coeFn {α : Type u} {β : Type v} [] :
Embedding (UniformFun.ofFun DFunLike.coe)
@[simp]
theorem BoundedContinuousFunction.const_apply (α : Type u) {β : Type v} [] (b : β) :
= fun (x : α) => b
@[simp]
theorem BoundedContinuousFunction.const_toFun (α : Type u) {β : Type v} [] (b : β) :
= fun (x : α) => b
def BoundedContinuousFunction.const (α : Type u) {β : Type v} [] (b : β) :

Constant as a continuous bounded function.

Equations
• = { toContinuousMap := , map_bounded' := }
Instances For
theorem BoundedContinuousFunction.const_apply' {α : Type u} {β : Type v} [] (a : α) (b : β) :
= b
instance BoundedContinuousFunction.instInhabited {α : Type u} {β : Type v} [] [] :

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

Equations
theorem BoundedContinuousFunction.lipschitz_evalx {α : Type u} {β : Type v} [] (x : α) :
LipschitzWith 1 fun (f : ) => f x
theorem BoundedContinuousFunction.continuous_coe {α : Type u} {β : Type v} [] :
Continuous fun (f : ) (x : α) => f x
theorem BoundedContinuousFunction.continuous_eval_const {α : Type u} {β : Type v} [] {x : α} :
Continuous fun (f : ) => f x

When x is fixed, (f : α →ᵇ β) ↦ f x is continuous.

theorem BoundedContinuousFunction.continuous_eval {α : Type u} {β : Type v} [] :
Continuous fun (p : ) => p.1 p.2

The evaluation map is continuous, as a joint function of u and x.

instance BoundedContinuousFunction.instCompleteSpace {α : Type u} {β : Type v} [] [] :

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

Equations
• =
def BoundedContinuousFunction.compContinuous {α : Type u} {β : Type v} [] {δ : Type u_2} [] (f : ) (g : C(δ, α)) :

Composition of a bounded continuous function and a continuous function.

Equations
• f.compContinuous g = { toContinuousMap := f.comp g, map_bounded' := }
Instances For
@[simp]
theorem BoundedContinuousFunction.coe_compContinuous {α : Type u} {β : Type v} [] {δ : Type u_2} [] (f : ) (g : C(δ, α)) :
(f.compContinuous g) = f g
@[simp]
theorem BoundedContinuousFunction.compContinuous_apply {α : Type u} {β : Type v} [] {δ : Type u_2} [] (f : ) (g : C(δ, α)) (x : δ) :
(f.compContinuous g) x = f (g x)
theorem BoundedContinuousFunction.lipschitz_compContinuous {α : Type u} {β : Type v} [] {δ : Type u_2} [] (g : C(δ, α)) :
LipschitzWith 1 fun (f : ) => f.compContinuous g
theorem BoundedContinuousFunction.continuous_compContinuous {α : Type u} {β : Type v} [] {δ : Type u_2} [] (g : C(δ, α)) :
Continuous fun (f : ) => f.compContinuous g
def BoundedContinuousFunction.restrict {α : Type u} {β : Type v} [] (f : ) (s : Set α) :

Restrict a bounded continuous function to a set.

Equations
• f.restrict s = f.compContinuous
Instances For
@[simp]
theorem BoundedContinuousFunction.coe_restrict {α : Type u} {β : Type v} [] (f : ) (s : Set α) :
(f.restrict s) = f Subtype.val
@[simp]
theorem BoundedContinuousFunction.restrict_apply {α : Type u} {β : Type v} [] (f : ) (s : Set α) (x : s) :
(f.restrict s) x = f x
def BoundedContinuousFunction.comp {α : Type u} {β : Type v} {γ : Type w} [] (G : βγ) {C : NNReal} (H : ) (f : ) :

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

Equations
• = { toFun := fun (x : α) => G (f x), continuous_toFun := , map_bounded' := }
Instances For
theorem BoundedContinuousFunction.lipschitz_comp {α : Type u} {β : Type v} {γ : Type w} [] {G : βγ} {C : NNReal} (H : ) :

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

theorem BoundedContinuousFunction.uniformContinuous_comp {α : Type u} {β : Type v} {γ : Type w} [] {G : βγ} {C : NNReal} (H : ) :

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

theorem BoundedContinuousFunction.continuous_comp {α : Type u} {β : Type v} {γ : Type w} [] {G : βγ} {C : NNReal} (H : ) :

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

def BoundedContinuousFunction.codRestrict {α : Type u} {β : Type v} [] (s : Set β) (f : ) (H : ∀ (x : α), f x s) :

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

Equations
• = { toFun := Set.codRestrict (f) s H, continuous_toFun := , map_bounded' := }
Instances For
def BoundedContinuousFunction.extend {α : Type u} {β : Type v} [] {δ : Type u_2} [] [] (f : α δ) (g : ) (h : ) :

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
• = { toFun := Function.extend f g h, continuous_toFun := , map_bounded' := }
Instances For
@[simp]
theorem BoundedContinuousFunction.extend_apply {α : Type u} {β : Type v} [] {δ : Type u_2} [] [] (f : α δ) (g : ) (h : ) (x : α) :
() (f x) = g x
@[simp]
theorem BoundedContinuousFunction.extend_comp {α : Type u} {β : Type v} [] {δ : Type u_2} [] [] (f : α δ) (g : ) (h : ) :
() f = g
theorem BoundedContinuousFunction.extend_apply' {α : Type u} {β : Type v} [] {δ : Type u_2} [] [] {f : α δ} {x : δ} (hx : x) (g : ) (h : ) :
() x = h x
theorem BoundedContinuousFunction.extend_of_empty {α : Type u} {β : Type v} [] {δ : Type u_2} [] [] [] (f : α δ) (g : ) (h : ) :
@[simp]
theorem BoundedContinuousFunction.dist_extend_extend {α : Type u} {β : Type v} [] {δ : Type u_2} [] [] (f : α δ) (g₁ : ) (g₂ : ) (h₁ : ) (h₂ : ) :
dist () () = max (dist g₁ g₂) (dist (h₁.restrict ()) (h₂.restrict ()))
theorem BoundedContinuousFunction.isometry_extend {α : Type u} {β : Type v} [] {δ : Type u_2} [] [] (f : α δ) (h : ) :
Isometry fun (g : ) =>
theorem BoundedContinuousFunction.arzela_ascoli₁ {α : Type u} {β : Type v} [] [] [] (A : ) (closed : ) (H : Equicontinuous fun (x : A) => x) :

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

theorem BoundedContinuousFunction.arzela_ascoli₂ {α : Type u} {β : Type v} [] [] (s : Set β) (hs : ) (A : ) (closed : ) (in_s : ∀ (f : ) (x : α), f Af x s) (H : Equicontinuous fun (x : A) => x) :

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

theorem BoundedContinuousFunction.arzela_ascoli {α : Type u} {β : Type v} [] [] [] (s : Set β) (hs : ) (A : ) (in_s : ∀ (f : ) (x : α), f Af x s) (H : Equicontinuous fun (x : A) => x) :

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

instance BoundedContinuousFunction.instZero {α : Type u} {β : Type v} [] [Zero β] :
Equations
• BoundedContinuousFunction.instZero = { zero := }
instance BoundedContinuousFunction.instOne {α : Type u} {β : Type v} [] [One β] :
Equations
• BoundedContinuousFunction.instOne = { one := }
@[simp]
theorem BoundedContinuousFunction.coe_zero {α : Type u} {β : Type v} [] [Zero β] :
0 = 0
@[simp]
theorem BoundedContinuousFunction.coe_one {α : Type u} {β : Type v} [] [One β] :
1 = 1
@[simp]
theorem BoundedContinuousFunction.mkOfCompact_zero {α : Type u} {β : Type v} [] [Zero β] [] :
@[simp]
theorem BoundedContinuousFunction.mkOfCompact_one {α : Type u} {β : Type v} [] [One β] [] :
theorem BoundedContinuousFunction.forall_coe_zero_iff_zero {α : Type u} {β : Type v} [] [Zero β] (f : ) :
(∀ (x : α), f x = 0) f = 0
theorem BoundedContinuousFunction.forall_coe_one_iff_one {α : Type u} {β : Type v} [] [One β] (f : ) :
(∀ (x : α), f x = 1) f = 1
@[simp]
theorem BoundedContinuousFunction.zero_compContinuous {α : Type u} {β : Type v} {γ : Type w} [] [Zero β] [] (f : C(γ, α)) :
@[simp]
theorem BoundedContinuousFunction.one_compContinuous {α : Type u} {β : Type v} {γ : Type w} [] [One β] [] (f : C(γ, α)) :
instance BoundedContinuousFunction.instAdd {α : Type u} {β : Type v} [] [] [] [] :

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

Equations
• BoundedContinuousFunction.instAdd = { add := fun (f g : ) => { toFun := fun (x : α) => f x + g x, continuous_toFun := , map_bounded' := } }
@[simp]
theorem BoundedContinuousFunction.coe_add {α : Type u} {β : Type v} [] [] [] [] (f : ) (g : ) :
(f + g) = f + g
theorem BoundedContinuousFunction.add_apply {α : Type u} {β : Type v} [] [] [] [] (f : ) (g : ) {x : α} :
(f + g) x = f x + g x
@[simp]
theorem BoundedContinuousFunction.mkOfCompact_add {α : Type u} {β : Type v} [] [] [] [] [] (f : C(α, β)) (g : C(α, β)) :
theorem BoundedContinuousFunction.add_compContinuous {α : Type u} {β : Type v} {γ : Type w} [] [] [] [] (f : ) (g : ) [] (h : C(γ, α)) :
(g + f).compContinuous h = g.compContinuous h + f.compContinuous h
@[simp]
theorem BoundedContinuousFunction.coe_nsmulRec {α : Type u} {β : Type v} [] [] [] [] (f : ) (n : ) :
(nsmulRec n f) = n f
instance BoundedContinuousFunction.instSMulNat {α : Type u} {β : Type v} [] [] [] [] :
Equations
• BoundedContinuousFunction.instSMulNat = { smul := fun (n : ) (f : ) => { toContinuousMap := n f.toContinuousMap, map_bounded' := } }
@[simp]
theorem BoundedContinuousFunction.coe_nsmul {α : Type u} {β : Type v} [] [] [] [] (r : ) (f : ) :
(r f) = r f
@[simp]
theorem BoundedContinuousFunction.nsmul_apply {α : Type u} {β : Type v} [] [] [] [] (r : ) (f : ) (v : α) :
(r f) v = r f v
instance BoundedContinuousFunction.instAddMonoid {α : Type u} {β : Type v} [] [] [] [] :
Equations
@[simp]
theorem BoundedContinuousFunction.coeFnAddHom_apply {α : Type u} {β : Type v} [] [] [] [] :
∀ (a : ) (a_1 : α), BoundedContinuousFunction.coeFnAddHom a a_1 = a a_1
def BoundedContinuousFunction.coeFnAddHom {α : Type u} {β : Type v} [] [] [] [] :
→+ αβ

Coercion of a NormedAddGroupHom is an AddMonoidHom. Similar to AddMonoidHom.coeFn.

Equations
• BoundedContinuousFunction.coeFnAddHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
Instances For
@[simp]
theorem BoundedContinuousFunction.toContinuousMapAddHom_apply (α : Type u) (β : Type v) [] [] [] [] (self : ) :
= self.toContinuousMap
def BoundedContinuousFunction.toContinuousMapAddHom (α : Type u) (β : Type v) [] [] [] [] :

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

Equations
• = { toFun := BoundedContinuousFunction.toContinuousMap, map_zero' := , map_add' := }
Instances For
theorem BoundedContinuousFunction.instAddAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [] [] [] [] (f : ) (g : ) :
f + g = g + f
instance BoundedContinuousFunction.instAddAddCommMonoid {α : Type u} {β : Type v} [] [] [] [] :
Equations
instance BoundedContinuousFunction.instAddCommMonoid {α : Type u} {β : Type v} [] [] [] [] :
Equations
@[simp]
theorem BoundedContinuousFunction.coe_sum {α : Type u} {β : Type v} [] [] [] [] {ι : Type u_2} (s : ) (f : ) :
(is, f i) = is, (f i)
theorem BoundedContinuousFunction.sum_apply {α : Type u} {β : Type v} [] [] [] [] {ι : Type u_2} (s : ) (f : ) (a : α) :
(is, f i) a = is, (f i) a
instance BoundedContinuousFunction.instLipschitzAdd {α : Type u} {β : Type v} [] [] [] :
Equations
• =
instance BoundedContinuousFunction.instSub {α : Type u} [] {R : Type u_2} [Sub R] [] [] :

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

Equations
• BoundedContinuousFunction.instSub = { sub := fun (f g : ) => { toFun := fun (x : α) => f x - g x, continuous_toFun := , map_bounded' := } }
theorem BoundedContinuousFunction.sub_apply {α : Type u} [] {R : Type u_2} [Sub R] [] [] (f : ) (g : ) {x : α} :
(f - g) x = f x - g x
@[simp]
theorem BoundedContinuousFunction.coe_sub {α : Type u} [] {R : Type u_2} [Sub R] [] [] (f : ) (g : ) :
(f - g) = f - g
instance BoundedContinuousFunction.instNatCast {α : Type u} [] {β : Type u_2} [] :
Equations
• BoundedContinuousFunction.instNatCast = { natCast := fun (n : ) => }
@[simp]
theorem BoundedContinuousFunction.natCast_apply {α : Type u} [] {β : Type u_2} [] (n : ) (x : α) :
n x = n
instance BoundedContinuousFunction.instIntCast {α : Type u} [] {β : Type u_2} [] :
Equations
• BoundedContinuousFunction.instIntCast = { intCast := fun (m : ) => }
@[simp]
theorem BoundedContinuousFunction.intCast_apply {α : Type u} [] {β : Type u_2} [] (m : ) (x : α) :
m x = m
instance BoundedContinuousFunction.instMul {α : Type u} [] {R : Type u_2} [Mul R] [] [] :
Equations
• BoundedContinuousFunction.instMul = { mul := fun (f g : ) => { toFun := fun (x : α) => f x * g x, continuous_toFun := , map_bounded' := } }
@[simp]
theorem BoundedContinuousFunction.coe_mul {α : Type u} [] {R : Type u_2} [Mul R] [] [] (f : ) (g : ) :
(f * g) = f * g
theorem BoundedContinuousFunction.mul_apply {α : Type u} [] {R : Type u_2} [Mul R] [] [] (f : ) (g : ) (x : α) :
(f * g) x = f x * g x
instance BoundedContinuousFunction.instPow {α : Type u} [] {R : Type u_2} [] [] [] :
Equations
• BoundedContinuousFunction.instPow = { pow := fun (f : ) (n : ) => { toFun := fun (x : α) => f x ^ n, continuous_toFun := , map_bounded' := } }
theorem BoundedContinuousFunction.coe_pow {α : Type u} [] {R : Type u_2} [] [] [] (n : ) (f : ) :
(f ^ n) = f ^ n
@[simp]
theorem BoundedContinuousFunction.pow_apply {α : Type u} [] {R : Type u_2} [] [] [] (n : ) (f : ) (x : α) :
(f ^ n) x = f x ^ n
instance BoundedContinuousFunction.instMonoid {α : Type u} [] {R : Type u_2} [] [] [] :
Equations
instance BoundedContinuousFunction.instCommMonoid {α : Type u} [] {R : Type u_2} [] [] [] :
Equations
• BoundedContinuousFunction.instCommMonoid = let __spread.0 := BoundedContinuousFunction.instMonoid;
instance BoundedContinuousFunction.instSemiring {α : Type u} [] {R : Type u_2} [] [] [] [] [] :
Equations
instance BoundedContinuousFunction.instNorm {α : Type u} {β : Type v} [] :
Equations
• BoundedContinuousFunction.instNorm = { norm := fun (x : ) => dist x 0 }
theorem BoundedContinuousFunction.norm_def {α : Type u} {β : Type v} [] (f : ) :
theorem BoundedContinuousFunction.norm_eq {α : Type u} {β : Type v} [] (f : ) :
f = sInf {C : | 0 C ∀ (x : α), f x C}

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.

theorem BoundedContinuousFunction.norm_eq_of_nonempty {α : Type u} {β : Type v} [] (f : ) [h : ] :
f = sInf {C : | ∀ (x : α), f x C}

When the domain is non-empty, we do not need the 0 ≤ C condition in the formula for ‖f‖ as a sInf.

@[simp]
theorem BoundedContinuousFunction.norm_eq_zero_of_empty {α : Type u} {β : Type v} [] (f : ) [] :
theorem BoundedContinuousFunction.norm_coe_le_norm {α : Type u} {β : Type v} [] (f : ) (x : α) :
theorem BoundedContinuousFunction.neg_norm_le_apply {α : Type u} [] (f : ) (x : α) :
theorem BoundedContinuousFunction.apply_le_norm {α : Type u} [] (f : ) (x : α) :
f x f
theorem BoundedContinuousFunction.dist_le_two_norm' {β : Type v} {γ : Type w} {f : γβ} {C : } (hC : ∀ (x : γ), f x C) (x : γ) (y : γ) :
dist (f x) (f y) 2 * C
theorem BoundedContinuousFunction.dist_le_two_norm {α : Type u} {β : Type v} [] (f : ) (x : α) (y : α) :
dist (f x) (f y) 2 * f

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

theorem BoundedContinuousFunction.norm_le {α : Type u} {β : Type v} [] {f : } {C : } (C0 : 0 C) :
f C ∀ (x : α), f x C

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

theorem BoundedContinuousFunction.norm_le_of_nonempty {α : Type u} {β : Type v} [] [] {f : } {M : } :
f M ∀ (x : α), f x M
theorem BoundedContinuousFunction.norm_lt_iff_of_compact {α : Type u} {β : Type v} [] [] {f : } {M : } (M0 : 0 < M) :
f < M ∀ (x : α), f x < M
theorem BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [] [] [] {f : } {M : } :
f < M ∀ (x : α), f x < M
theorem BoundedContinuousFunction.norm_const_le {α : Type u} {β : Type v} [] (b : β) :

Norm of const α b is less than or equal to ‖b‖. If α is nonempty, then it is equal to ‖b‖.

@[simp]
theorem BoundedContinuousFunction.norm_const_eq {α : Type u} {β : Type v} [] [h : ] (b : β) :
def BoundedContinuousFunction.ofNormedAddCommGroup {α : Type u} {β : Type v} [] (f : αβ) (Hf : ) (C : ) (H : ∀ (x : α), f x C) :

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

Equations
• = { toFun := fun (n : α) => f n, continuous_toFun := Hf, map_bounded' := }
Instances For
@[simp]
theorem BoundedContinuousFunction.coe_ofNormedAddCommGroup {α : Type u} {β : Type v} [] (f : αβ) (Hf : ) (C : ) (H : ∀ (x : α), f x C) :
= f
theorem BoundedContinuousFunction.norm_ofNormedAddCommGroup_le {α : Type u} {β : Type v} [] {f : αβ} (hfc : ) {C : } (hC : 0 C) (hfC : ∀ (x : α), f x C) :
def BoundedContinuousFunction.ofNormedAddCommGroupDiscrete {α : Type u} {β : Type v} [] [] (f : αβ) (C : ) (H : ∀ (x : α), f x C) :

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

Equations
Instances For
@[simp]
theorem BoundedContinuousFunction.coe_ofNormedAddCommGroupDiscrete {α : Type u} {β : Type v} [] [] (f : αβ) (C : ) (H : ∀ (x : α), f x C) :
def BoundedContinuousFunction.normComp {α : Type u} {β : Type v} [] (f : ) :

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 =
Instances For
@[simp]
theorem BoundedContinuousFunction.coe_normComp {α : Type u} {β : Type v} [] (f : ) :
f.normComp = norm f
@[simp]
theorem BoundedContinuousFunction.norm_normComp {α : Type u} {β : Type v} [] (f : ) :
f.normComp = f
theorem BoundedContinuousFunction.bddAbove_range_norm_comp {α : Type u} {β : Type v} [] (f : ) :
BddAbove (Set.range (norm f))
theorem BoundedContinuousFunction.norm_eq_iSup_norm {α : Type u} {β : Type v} [] (f : ) :
f = ⨆ (x : α), f x
instance BoundedContinuousFunction.instNormOneClass {α : Type u} {β : Type v} [] [] [One β] [] :

If ‖(1 : β)‖ = 1, then ‖(1 : α →ᵇ β)‖ = 1 if α is nonempty.

Equations
• =
instance BoundedContinuousFunction.instNeg {α : Type u} {β : Type v} [] :

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

Equations
• BoundedContinuousFunction.instNeg = { neg := fun (f : ) => }
@[simp]
theorem BoundedContinuousFunction.coe_neg {α : Type u} {β : Type v} [] (f : ) :
(-f) = -f
theorem BoundedContinuousFunction.neg_apply {α : Type u} {β : Type v} [] (f : ) {x : α} :
(-f) x = -f x
@[simp]
theorem BoundedContinuousFunction.mkOfCompact_neg {α : Type u} {β : Type v} [] [] (f : C(α, β)) :
@[simp]
theorem BoundedContinuousFunction.mkOfCompact_sub {α : Type u} {β : Type v} [] [] (f : C(α, β)) (g : C(α, β)) :
@[simp]
theorem BoundedContinuousFunction.coe_zsmulRec {α : Type u} {β : Type v} [] (f : ) (z : ) :
(zsmulRec (fun (x : ) (x_1 : ) => x x_1) z f) = z f
instance BoundedContinuousFunction.instSMulInt {α : Type u} {β : Type v} [] :
Equations
• BoundedContinuousFunction.instSMulInt = { smul := fun (n : ) (f : ) => { toContinuousMap := n f.toContinuousMap, map_bounded' := } }
@[simp]
theorem BoundedContinuousFunction.coe_zsmul {α : Type u} {β : Type v} [] (r : ) (f : ) :
(r f) = r f
@[simp]
theorem BoundedContinuousFunction.zsmul_apply {α : Type u} {β : Type v} [] (r : ) (f : ) (v : α) :
(r f) v = r f v
instance BoundedContinuousFunction.instAddCommGroup {α : Type u} {β : Type v} [] :
Equations
Equations
instance BoundedContinuousFunction.instNormedAddCommGroup {α : Type u_2} {β : Type u_3} [] :
Equations
theorem BoundedContinuousFunction.nnnorm_def {α : Type u} {β : Type v} [] (f : ) :
theorem BoundedContinuousFunction.nnnorm_coe_le_nnnorm {α : Type u} {β : Type v} [] (f : ) (x : α) :
theorem BoundedContinuousFunction.nndist_le_two_nnnorm {α : Type u} {β : Type v} [] (f : ) (x : α) (y : α) :
nndist (f x) (f y) 2 * f‖₊
theorem BoundedContinuousFunction.nnnorm_le {α : Type u} {β : Type v} [] (f : ) (C : NNReal) :
f‖₊ C ∀ (x : α), f x‖₊ C

The nnnorm of a function is controlled by the supremum of the pointwise nnnorms.

theorem BoundedContinuousFunction.nnnorm_const_le {α : Type u} {β : Type v} [] (b : β) :
@[simp]
theorem BoundedContinuousFunction.nnnorm_const_eq {α : Type u} {β : Type v} [] [] (b : β) :
theorem BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm {α : Type u} {β : Type v} [] (f : ) :
f‖₊ = ⨆ (x : α), f x‖₊
theorem BoundedContinuousFunction.abs_diff_coe_le_dist {α : Type u} {β : Type v} [] (f : ) (g : ) {x : α} :
f x - g x dist f g
theorem BoundedContinuousFunction.coe_le_coe_add_dist {α : Type u} [] {x : α} {f : } {g : } :
f x g x + dist f g
theorem BoundedContinuousFunction.norm_compContinuous_le {α : Type u} {β : Type v} {γ : Type w} [] [] (f : ) (g : C(γ, α)) :
f.compContinuous g f

### 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.

instance BoundedContinuousFunction.instSMul {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [] :
Equations
• BoundedContinuousFunction.instSMul = { smul := fun (c : 𝕜) (f : ) => { toContinuousMap := c f.toContinuousMap, map_bounded' := } }
@[simp]
theorem BoundedContinuousFunction.coe_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [] (c : 𝕜) (f : ) :
(c f) = fun (x : α) => c f x
theorem BoundedContinuousFunction.smul_apply {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [] (c : 𝕜) (f : ) (x : α) :
(c f) x = c f x
instance BoundedContinuousFunction.instIsCentralScalar {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [] [SMul 𝕜ᵐᵒᵖ β] [] :
Equations
• =
instance BoundedContinuousFunction.instBoundedSMul {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [Zero 𝕜] [Zero β] [SMul 𝕜 β] [] :
Equations
• =
instance BoundedContinuousFunction.instMulAction {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [] [Zero β] [] [] :
Equations
instance BoundedContinuousFunction.instDistribMulAction {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [] [] [] [] [] [] :
Equations
instance BoundedContinuousFunction.instModule {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [] [] [Module 𝕜 β] [] [] [] :
Equations
• BoundedContinuousFunction.instModule = Function.Injective.module 𝕜 { toFun := DFunLike.coe, map_zero' := , map_add' := }
def BoundedContinuousFunction.evalCLM {α : Type u} {β : Type v} (𝕜 : Type u_2) [] [] [] [Module 𝕜 β] [] [] [] (x : α) :

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

Equations
• = { toFun := fun (f : ) => f x, map_add' := , map_smul' := , cont := }
Instances For
@[simp]
theorem BoundedContinuousFunction.evalCLM_apply {α : Type u} {β : Type v} (𝕜 : Type u_2) [] [] [] [Module 𝕜 β] [] [] [] (x : α) (f : ) :
= f x
@[simp]
theorem BoundedContinuousFunction.toContinuousMapLinearMap_apply (α : Type u) (β : Type v) (𝕜 : Type u_2) [] [] [] [Module 𝕜 β] [] [] [] (self : ) :
= self.toContinuousMap
def BoundedContinuousFunction.toContinuousMapLinearMap (α : Type u) (β : Type v) (𝕜 : Type u_2) [] [] [] [Module 𝕜 β] [] [] [] :

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

Equations
• = { 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.

instance BoundedContinuousFunction.instNormedSpace {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [] [] :
Equations
• BoundedContinuousFunction.instNormedSpace =
def ContinuousLinearMap.compLeftContinuousBounded (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_2} [] [] [] (g : β →L[𝕜] γ) :

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
@[simp]
theorem ContinuousLinearMap.compLeftContinuousBounded_apply (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_2} [] [] [] (g : β →L[𝕜] γ) (f : ) (x : α) :
= g (f x)

### 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.

instance BoundedContinuousFunction.instNonUnitalRing {α : Type u} [] {R : Type u_2} :
Equations
Equations
• BoundedContinuousFunction.instNonUnitalSeminormedRing = let __src := BoundedContinuousFunction.instSeminormedAddCommGroup;
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BoundedContinuousFunction.coe_npowRec {α : Type u} [] {R : Type u_2} [] (f : ) (n : ) :
(npowRec n f) = f ^ n
instance BoundedContinuousFunction.hasNatPow {α : Type u} [] {R : Type u_2} [] :
Equations
• BoundedContinuousFunction.hasNatPow = { pow := fun (f : ) (n : ) => { toContinuousMap := f.toContinuousMap ^ n, map_bounded' := } }
instance BoundedContinuousFunction.instNatCast_1 {α : Type u} [] {R : Type u_2} [] :
Equations
• BoundedContinuousFunction.instNatCast_1 = { natCast := fun (n : ) => }
@[simp]
theorem BoundedContinuousFunction.coe_natCast {α : Type u} [] {R : Type u_2} [] (n : ) :
n = n
@[simp]
theorem BoundedContinuousFunction.coe_ofNat {α : Type u} [] {R : Type u_2} [] (n : ) [n.AtLeastTwo] :
(OfNat.ofNat n) =
instance BoundedContinuousFunction.instIntCast_1 {α : Type u} [] {R : Type u_2} [] :
Equations
• BoundedContinuousFunction.instIntCast_1 = { intCast := fun (n : ) => }
@[simp]
theorem BoundedContinuousFunction.coe_intCast {α : Type u} [] {R : Type u_2} [] (n : ) :
n = n
instance BoundedContinuousFunction.instRing {α : Type u} [] {R : Type u_2} [] :
Equations
• BoundedContinuousFunction.instRing = Function.Injective.ring (fun (f : ) => f)
instance BoundedContinuousFunction.instSeminormedRing {α : Type u} [] {R : Type u_2} [] :
Equations
• One or more equations did not get rendered due to their size.
instance BoundedContinuousFunction.instNormedRing {α : Type u} [] {R : Type u_2} [] :
Equations

### 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.

instance BoundedContinuousFunction.instCommRing {α : Type u} [] {R : Type u_2} :
Equations
• BoundedContinuousFunction.instCommRing =
Equations
• One or more equations did not get rendered due to their size.
instance BoundedContinuousFunction.instNormedCommRing {α : Type u} [] {R : Type u_2} [] :
Equations

### 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.

def BoundedContinuousFunction.C {α : Type u} {γ : Type w} {𝕜 : Type u_2} [] [] [] [] :

BoundedContinuousFunction.const as a RingHom.

Equations
• BoundedContinuousFunction.C = { toFun := fun (c : 𝕜) => BoundedContinuousFunction.const α (() c), map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
instance BoundedContinuousFunction.instAlgebra {α : Type u} {γ : Type w} {𝕜 : Type u_2} [] [] [] [] :
Equations
• BoundedContinuousFunction.instAlgebra = Algebra.mk BoundedContinuousFunction.C
@[simp]
theorem BoundedContinuousFunction.algebraMap_apply {α : Type u} {γ : Type w} {𝕜 : Type u_2} [] [] [] [] (k : 𝕜) (a : α) :
(() k) a = k 1
instance BoundedContinuousFunction.instNormedAlgebra {α : Type u} {γ : Type w} {𝕜 : Type u_2} [] [] [] [] :
Equations

### 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 𝕜.

instance BoundedContinuousFunction.instSMul' {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
instance BoundedContinuousFunction.instModule' {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [] [] :
Equations
• BoundedContinuousFunction.instModule' =
instance BoundedContinuousFunction.instBoundedSMul_1 {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [] [] :
Equations
• =
theorem BoundedContinuousFunction.NNReal.upper_bound {α : Type u_2} [] (f : ) (x : α) :
f x nndist f 0

### 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).

instance BoundedContinuousFunction.instStarAddMonoid {α : Type u} {β : Type v} [] [] [] :
Equations
@[simp]
theorem BoundedContinuousFunction.coe_star {α : Type u} {β : Type v} [] [] [] (f : ) :
(star f) = star f

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.

@[simp]
theorem BoundedContinuousFunction.star_apply {α : Type u} {β : Type v} [] [] [] (f : ) (x : α) :
(star f) x = star (f x)
instance BoundedContinuousFunction.instNormedStarGroup {α : Type u} {β : Type v} [] [] [] :
Equations
• =
instance BoundedContinuousFunction.instStarModule {α : Type u} {β : Type v} {𝕜 : Type u_2} [] [] [] [] [] [] [] :
Equations
• =
instance BoundedContinuousFunction.instStarRing {α : Type u} {β : Type v} [] [] [] :
Equations
instance BoundedContinuousFunction.instCstarRing {α : Type u} {β : Type v} [] [] [] :
Equations
• =
instance BoundedContinuousFunction.instPartialOrder {α : Type u} {β : Type v} [] :
Equations
• BoundedContinuousFunction.instPartialOrder = PartialOrder.lift (fun (f : ) => f.toFun)
instance BoundedContinuousFunction.instSup {α : Type u} {β : Type v} [] :
Equations
• BoundedContinuousFunction.instSup = { sup := fun (f g : ) => { toFun := f g, continuous_toFun := , map_bounded' := } }
instance BoundedContinuousFunction.instInf {α : Type u} {β : Type v} [] :
Equations
• BoundedContinuousFunction.instInf = { inf := fun (f g : ) => { toFun := f g, continuous_toFun := , map_bounded' := } }
@[simp]
theorem BoundedContinuousFunction.coe_sup {α : Type u} {β : Type v} [] (f : ) (g : ) :
(f g) = f g
@[simp]
theorem BoundedContinuousFunction.coe_inf {α : Type u} {β : Type v} [] (f : ) (g : ) :
(f g) = f g
Equations
Equations
instance BoundedContinuousFunction.instLattice {α : Type u} {β : Type v} [] :
Equations
@[simp]
theorem BoundedContinuousFunction.coe_abs {α : Type u} {β : Type v} [] (f : ) :
|f| = |f|
@[simp]
theorem BoundedContinuousFunction.coe_posPart {α : Type u} {β : Type v} [] (f : ) :
f = (f)
@[simp]
theorem BoundedContinuousFunction.coe_negPart {α : Type u} {β : Type v} [] (f : ) :
f = (f)
@[deprecated BoundedContinuousFunction.coe_sup]
theorem BoundedContinuousFunction.coeFn_sup {α : Type u} {β : Type v} [] (f : ) (g : ) :
(f g) = f g

Alias of BoundedContinuousFunction.coe_sup.

@[deprecated BoundedContinuousFunction.coe_abs]
theorem BoundedContinuousFunction.coeFn_abs {α : Type u} {β : Type v} [] (f : ) :
|f| = |f|

Alias of BoundedContinuousFunction.coe_abs.

Equations

The nonnegative part of a bounded continuous ℝ-valued function as a bounded continuous ℝ≥0-valued function.

Equations
Instances For
@[simp]
theorem BoundedContinuousFunction.nnrealPart_coeFn_eq {α : Type u} [] (f : ) :
f.nnrealPart =
def BoundedContinuousFunction.nnnorm {α : Type u} [] (f : ) :

The absolute value of a bounded continuous ℝ-valued function as a bounded continuous ℝ≥0-valued function.

Equations
• f.nnnorm =
Instances For
@[simp]
theorem BoundedContinuousFunction.nnnorm_coeFn_eq {α : Type u} [] (f : ) :
f.nnnorm = nnnorm f
theorem BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg {α : Type u} [] (f : ) :
f = NNReal.toReal f.nnrealPart - NNReal.toReal (-f).nnrealPart

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

theorem BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg {α : Type u} [] (f : ) :
abs f = NNReal.toReal f.nnrealPart + NNReal.toReal (-f).nnrealPart

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