Inheritance of normed algebraic structures by bounded continuous functions

For various types of normed algebraic structures β, we show in this file that the space of bounded continuous functions from α to β inherits the same normed structure, by using pointwise operations and checking that they are compatible with the uniform distance.

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : Norm (BoundedContinuousFunction α β)

Equations

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

theorem BoundedContinuousFunction.norm_def {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖ = dist f 0

theorem BoundedContinuousFunction.norm_eq {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖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} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) [h : Nonempty α] : ‖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} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) [IsEmpty α] : ‖f‖ = 0

theorem BoundedContinuousFunction.norm_coe_le_norm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (x : α) : ‖f x‖ ≤ ‖f‖

theorem BoundedContinuousFunction.neg_norm_le_apply {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) (x : α) : -‖f‖ ≤ f x

theorem BoundedContinuousFunction.apply_le_norm {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) (x : α) : f x ≤ ‖f‖

theorem BoundedContinuousFunction.dist_le_two_norm' {β : Type v} {γ : Type w} [SeminormedAddCommGroup β] {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} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (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} [TopologicalSpace α] [SeminormedAddCommGroup β] {f : BoundedContinuousFunction α β} {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} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] {f : BoundedContinuousFunction α β} {M : ℝ} : ‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M

theorem BoundedContinuousFunction.norm_lt_iff_of_compact {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [CompactSpace α] {f : BoundedContinuousFunction α β} {M : ℝ} (M0 : 0 < M) : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] [CompactSpace α] {f : BoundedContinuousFunction α β} {M : ℝ} : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem BoundedContinuousFunction.norm_const_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (b : β) : ‖const α b‖ ≤ ‖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} [TopologicalSpace α] [SeminormedAddCommGroup β] [h : Nonempty α] (b : β) : ‖const α b‖ = ‖b‖

def BoundedContinuousFunction.ofNormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : α → β) (Hf : Continuous f) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) : BoundedContinuousFunction α β

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' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.coe_ofNormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : α → β) (Hf : Continuous f) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) : ⇑(ofNormedAddCommGroup f Hf C H) = f

theorem BoundedContinuousFunction.norm_ofNormedAddCommGroup_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] {f : α → β} (hfc : Continuous f) {C : ℝ} (hC : 0 ≤ C) (hfC : ∀ (x : α), ‖f x‖ ≤ C) : ‖ofNormedAddCommGroup f hfc C hfC‖ ≤ C

def BoundedContinuousFunction.ofNormedAddCommGroupDiscrete {α : Type u} {β : Type v} [TopologicalSpace α] [DiscreteTopology α] [SeminormedAddCommGroup β] (f : α → β) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) : BoundedContinuousFunction α β

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

Equations

• BoundedContinuousFunction.ofNormedAddCommGroupDiscrete f C H = BoundedContinuousFunction.ofNormedAddCommGroup f ⋯ C H

@[simp]

theorem BoundedContinuousFunction.coe_ofNormedAddCommGroupDiscrete {α : Type u} {β : Type v} [TopologicalSpace α] [DiscreteTopology α] [SeminormedAddCommGroup β] (f : α → β) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C) : ⇑(ofNormedAddCommGroupDiscrete f C H) = f

def BoundedContinuousFunction.normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : BoundedContinuousFunction α ℝ

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

@[simp]

theorem BoundedContinuousFunction.coe_normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ⇑f.normComp = norm ∘ ⇑f

@[simp]

theorem BoundedContinuousFunction.norm_normComp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f.normComp‖ = ‖f‖

theorem BoundedContinuousFunction.bddAbove_range_norm_comp {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : BddAbove (Set.range (norm ∘ ⇑f))

theorem BoundedContinuousFunction.norm_eq_iSup_norm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖ = ⨆ (x : α), ‖f x‖

instance BoundedContinuousFunction.instNormOneClass {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] [One β] [NormOneClass β] : NormOneClass (BoundedContinuousFunction α β)

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNeg {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : Neg (BoundedContinuousFunction α β)

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

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_neg {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ⇑(-f) = -⇑f

theorem BoundedContinuousFunction.neg_apply {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) {x : α} : (-f) x = -f x

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_neg {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [CompactSpace α] (f : C(α, β)) : mkOfCompact (-f) = -mkOfCompact f

@[simp]

theorem BoundedContinuousFunction.mkOfCompact_sub {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [CompactSpace α] (f g : C(α, β)) : mkOfCompact (f - g) = mkOfCompact f - mkOfCompact g

@[simp]

theorem BoundedContinuousFunction.coe_zsmulRec {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (z : ℤ) : ⇑(zsmulRec (fun (x1 : ℕ) (x2 : BoundedContinuousFunction α β) => x1 • x2) z f) = z • ⇑f

@[implicit_reducible]

instance BoundedContinuousFunction.instSMulInt {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : SMul ℤ (BoundedContinuousFunction α β)

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_zsmul {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (r : ℤ) (f : BoundedContinuousFunction α β) : ⇑(r • f) = r • ⇑f

@[simp]

theorem BoundedContinuousFunction.zsmul_apply {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (r : ℤ) (f : BoundedContinuousFunction α β) (v : α) : (r • f) v = r • f v

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : AddCommGroup (BoundedContinuousFunction α β)

Equations

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instSeminormedAddCommGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] : SeminormedAddCommGroup (BoundedContinuousFunction α β)

Equations

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNormedAddCommGroup {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [NormedAddCommGroup β] : NormedAddCommGroup (BoundedContinuousFunction α β)

Equations

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

theorem BoundedContinuousFunction.nnnorm_def {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖₊ = nndist f 0

theorem BoundedContinuousFunction.nnnorm_coe_le_nnnorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (x : α) : ‖f x‖₊ ≤ ‖f‖₊

theorem BoundedContinuousFunction.nndist_le_two_nnnorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (x y : α) : nndist (f x) (f y) ≤ 2 * ‖f‖₊

theorem BoundedContinuousFunction.nnnorm_le {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) (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} [TopologicalSpace α] [SeminormedAddCommGroup β] (b : β) : ‖const α b‖₊ ≤ ‖b‖₊

@[simp]

theorem BoundedContinuousFunction.nnnorm_const_eq {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [Nonempty α] (b : β) : ‖const α b‖₊ = ‖b‖₊

theorem BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖₊ = ⨆ (x : α), ‖f x‖₊

theorem BoundedContinuousFunction.enorm_eq_iSup_enorm {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f : BoundedContinuousFunction α β) : ‖f‖ₑ = ⨆ (x : α), ‖f x‖ₑ

theorem BoundedContinuousFunction.abs_diff_coe_le_dist {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] (f g : BoundedContinuousFunction α β) {x : α} : ‖f x - g x‖ ≤ dist f g

theorem BoundedContinuousFunction.coe_le_coe_add_dist {α : Type u} [TopologicalSpace α] {x : α} {f g : BoundedContinuousFunction α ℝ} : f x ≤ g x + dist f g

theorem BoundedContinuousFunction.norm_compContinuous_le {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [SeminormedAddCommGroup β] [TopologicalSpace γ] (f : BoundedContinuousFunction α β) (g : C(γ, α)) : ‖f.compContinuous g‖ ≤ ‖f‖

@[implicit_reducible]

instance BoundedContinuousFunction.instNormedSpace {α : Type u} {β : Type v} {𝕜 : Type u_1} [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedField 𝕜] [NormedSpace 𝕜 β] : NormedSpace 𝕜 (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instNormedSpace = { toModule := BoundedContinuousFunction.instModule, norm_smul_le := ⋯ }

noncomputable def ContinuousLinearMap.compLeftContinuousBounded (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_1} [TopologicalSpace α] [SeminormedAddCommGroup β] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 β] [SeminormedAddCommGroup γ] [NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) : BoundedContinuousFunction α β →L[𝕜] BoundedContinuousFunction α γ

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.

@[simp]

theorem ContinuousLinearMap.compLeftContinuousBounded_apply (α : Type u) {β : Type v} {γ : Type w} {𝕜 : Type u_1} [TopologicalSpace α] [SeminormedAddCommGroup β] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 β] [SeminormedAddCommGroup γ] [NormedSpace 𝕜 γ] (g : β →L[𝕜] γ) (f : BoundedContinuousFunction α β) (x : α) : ((ContinuousLinearMap.compLeftContinuousBounded α g) f) x = g (f x)

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNonUnitalRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalSeminormedRing R] : NonUnitalRing (BoundedContinuousFunction α R)

Equations

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNonUnitalSeminormedRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalSeminormedRing R] : NonUnitalSeminormedRing (BoundedContinuousFunction α R)

Equations

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

theorem BoundedContinuousFunction.norm_add_eq_max {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalSeminormedRing R] [IsCancelMulZero R] {f g : BoundedContinuousFunction α R} (h : f * g = 0) : ‖f + g‖ = max ‖f‖ ‖g‖

If the product of bounded continuous functions is zero, then the norm of their sum is the maximum of their norms.

theorem BoundedContinuousFunction.nnnorm_add_eq_max {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalSeminormedRing R] [IsCancelMulZero R] {f g : BoundedContinuousFunction α R} (h : f * g = 0) : ‖f + g‖₊ = max ‖f‖₊ ‖g‖₊

If the product of bounded continuous functions is zero, then the norm of their sum is the maximum of their norms.

theorem BoundedContinuousFunction.norm_sub_eq_max {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalSeminormedRing R] [IsCancelMulZero R] {f g : BoundedContinuousFunction α R} (h : f * g = 0) : ‖f - g‖ = max ‖f‖ ‖g‖

theorem BoundedContinuousFunction.nnnorm_sub_eq_max {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalSeminormedRing R] [IsCancelMulZero R] {f g : BoundedContinuousFunction α R} (h : f * g = 0) : ‖f - g‖₊ = max ‖f‖₊ ‖g‖₊

theorem BoundedContinuousFunction.nnnorm_sum_eq_sup {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalSeminormedRing R] [IsCancelMulZero R] {ι : Type u_2} {f : ι → BoundedContinuousFunction α R} (s : Finset ι) (h : Pairwise (Function.onFun (fun (x1 x2 : BoundedContinuousFunction α R) => x1 * x2 = 0) f)) : ‖∑ i ∈ s, f i‖₊ = s.sup fun (x : ι) => ‖f x‖₊

If the pairwise products of bounded continuous functions are all zero, then the norm of their sum is the maximum of their norms.

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNonUnitalSeminormedCommRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalSeminormedCommRing R] : NonUnitalSeminormedCommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNonUnitalSeminormedCommRing = { toNonUnitalSeminormedRing := BoundedContinuousFunction.instNonUnitalSeminormedRing, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNonUnitalNormedRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalNormedRing R] : NonUnitalNormedRing (BoundedContinuousFunction α R)

Equations

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNonUnitalNormedCommRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [NonUnitalNormedCommRing R] : NonUnitalNormedCommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instNonUnitalNormedCommRing = { toNonUnitalNormedRing := BoundedContinuousFunction.instNonUnitalNormedRing, mul_comm := ⋯ }

@[simp]

theorem BoundedContinuousFunction.coe_npowRec {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] (f : BoundedContinuousFunction α R) (n : ℕ) : ⇑(npowRec n f) = ⇑f ^ n

@[implicit_reducible]

instance BoundedContinuousFunction.hasNatPow {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] : Pow (BoundedContinuousFunction α R) ℕ

Equations

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

@[implicit_reducible]

instance BoundedContinuousFunction.instNatCast_1 {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] : NatCast (BoundedContinuousFunction α R)

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_natCast {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] (n : ℕ) : ⇑↑n = ↑n

@[simp]

theorem BoundedContinuousFunction.coe_ofNat {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] (n : ℕ) [n.AtLeastTwo] : ⇑(OfNat.ofNat n) = OfNat.ofNat n

@[implicit_reducible]

instance BoundedContinuousFunction.instIntCast_1 {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] : IntCast (BoundedContinuousFunction α R)

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_intCast {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] (n : ℤ) : ⇑↑n = ↑n

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] : Ring (BoundedContinuousFunction α R)

Equations

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instSeminormedRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedRing R] : SeminormedRing (BoundedContinuousFunction α R)

Equations

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

def RingHom.compLeftContinuousBounded {β : Type v} {γ : Type w} (α : Type u_2) [TopologicalSpace α] [SeminormedRing β] [SeminormedRing γ] (g : β →+* γ) {C : NNReal} (hg : LipschitzWith C ⇑g) : BoundedContinuousFunction α β →+* BoundedContinuousFunction α γ

Composition on the left by a (lipschitz-continuous) homomorphism of topological semirings, as a RingHom. Similar to RingHom.compLeftContinuous.

Equations

• RingHom.compLeftContinuousBounded α g hg = { toMonoidHom := MonoidHom.compLeftContinuousBounded α (↑g) hg, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.compLeftContinuousBounded_apply_apply {β : Type v} {γ : Type w} (α : Type u_2) [TopologicalSpace α] [SeminormedRing β] [SeminormedRing γ] (g : β →+* γ) {C : NNReal} (hg : LipschitzWith C ⇑g) (f : BoundedContinuousFunction α β) (x : α) : ((RingHom.compLeftContinuousBounded α g hg) f) x = g (f x)

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNormedRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [NormedRing R] : NormedRing (BoundedContinuousFunction α R)

Equations

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instCommRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedCommRing R] : CommRing (BoundedContinuousFunction α R)

Equations

• BoundedContinuousFunction.instCommRing = { toRing := BoundedContinuousFunction.instRing, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instSeminormedCommRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [SeminormedCommRing R] : SeminormedCommRing (BoundedContinuousFunction α R)

Equations

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instNormedCommRing {α : Type u} [TopologicalSpace α] {R : Type u_1} [NormedCommRing R] : NormedCommRing (BoundedContinuousFunction α R)

Equations

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

instance BoundedContinuousFunction.instIsScalarTower_1 {α : Type u} {β : Type v} {𝕜 : Type u_1} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [NonUnitalSeminormedRing β] [Zero 𝕜] [SMul 𝕜 β] [IsBoundedSMul 𝕜 β] [IsScalarTower 𝕜 β β] : IsScalarTower 𝕜 (BoundedContinuousFunction α β) (BoundedContinuousFunction α β)

instance BoundedContinuousFunction.instSMulCommClass_1 {α : Type u} {β : Type v} {𝕜 : Type u_1} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [NonUnitalSeminormedRing β] [Zero 𝕜] [SMul 𝕜 β] [IsBoundedSMul 𝕜 β] [SMulCommClass 𝕜 β β] : SMulCommClass 𝕜 (BoundedContinuousFunction α β) (BoundedContinuousFunction α β)

instance BoundedContinuousFunction.instSMulCommClass_2 {α : Type u} {β : Type v} {𝕜 : Type u_1} [PseudoMetricSpace 𝕜] [TopologicalSpace α] [NonUnitalSeminormedRing β] [Zero 𝕜] [SMul 𝕜 β] [IsBoundedSMul 𝕜 β] [SMulCommClass 𝕜 β β] : SMulCommClass (BoundedContinuousFunction α β) 𝕜 (BoundedContinuousFunction α β)

def BoundedContinuousFunction.C {α : Type u} {γ : Type w} {𝕜 : Type u_1} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] : 𝕜 →+* BoundedContinuousFunction α γ

BoundedContinuousFunction.const as a RingHom.

Equations

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

@[implicit_reducible]

instance BoundedContinuousFunction.instAlgebra {α : Type u} {γ : Type w} {𝕜 : Type u_1} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] : Algebra 𝕜 (BoundedContinuousFunction α γ)

Equations

• BoundedContinuousFunction.instAlgebra = { toSMul := BoundedContinuousFunction.instSMul, algebraMap := BoundedContinuousFunction.C, commutes' := ⋯, smul_def' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.algebraMap_apply {α : Type u} {γ : Type w} {𝕜 : Type u_1} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] (k : 𝕜) (a : α) : ((algebraMap 𝕜 (BoundedContinuousFunction α γ)) k) a = k • 1

@[implicit_reducible]

instance BoundedContinuousFunction.instNormedAlgebra {α : Type u} {γ : Type w} {𝕜 : Type u_1} [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] : NormedAlgebra 𝕜 (BoundedContinuousFunction α γ)

Equations

• BoundedContinuousFunction.instNormedAlgebra = { toAlgebra := BoundedContinuousFunction.instAlgebra, norm_smul_le := ⋯ }

def BoundedContinuousFunction.AlgHom.compLeftContinuousBounded {α : Type u} {β : Type v} {γ : Type w} (𝕜 : Type u_1) [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] [NormedRing β] [NormedAlgebra 𝕜 β] (g : β →ₐ[𝕜] γ) {C : NNReal} (hg : LipschitzWith C ⇑g) : BoundedContinuousFunction α β →ₐ[𝕜] BoundedContinuousFunction α γ

Composition on the left by a (lipschitz-continuous) homomorphism of topological R-algebras, as an AlgHom. Similar to AlgHom.compLeftContinuous.

Equations

• BoundedContinuousFunction.AlgHom.compLeftContinuousBounded 𝕜 g hg = { toRingHom := RingHom.compLeftContinuousBounded α g.toRingHom hg, commutes' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.AlgHom.compLeftContinuousBounded_apply_apply {α : Type u} {β : Type v} {γ : Type w} (𝕜 : Type u_1) [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] [NormedRing β] [NormedAlgebra 𝕜 β] (g : β →ₐ[𝕜] γ) {C : NNReal} (hg : LipschitzWith C ⇑g) (f : BoundedContinuousFunction α β) (x : α) : ((AlgHom.compLeftContinuousBounded 𝕜 g hg) f) x = g (f x)

def BoundedContinuousFunction.toContinuousMapₐ {α : Type u} {γ : Type w} (𝕜 : Type u_1) [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] : BoundedContinuousFunction α γ →ₐ[𝕜] C(α, γ)

The algebra-homomorphism forgetting that a bounded continuous function is bounded.

Equations

• BoundedContinuousFunction.toContinuousMapₐ 𝕜 = { toFun := toContinuousMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.toContinuousMapₐ_apply {α : Type u} {γ : Type w} (𝕜 : Type u_1) [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] (f : BoundedContinuousFunction α γ) : (toContinuousMapₐ 𝕜) f = ↑f

@[simp]

theorem BoundedContinuousFunction.coe_toContinuousMapₐ {α : Type u} {γ : Type w} (𝕜 : Type u_1) [NormedField 𝕜] [TopologicalSpace α] [NormedRing γ] [NormedAlgebra 𝕜 γ] (f : BoundedContinuousFunction α γ) : ⇑((toContinuousMapₐ 𝕜) f) = ⇑f

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instSMul' {α : Type u} {β : Type v} {𝕜 : Type u_1} [NormedField 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] : SMul (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

Equations

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

@[implicit_reducible]

noncomputable instance BoundedContinuousFunction.instModule' {α : Type u} {β : Type v} {𝕜 : Type u_1} [NormedField 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] : Module (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

Equations

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

instance BoundedContinuousFunction.instIsBoundedSMul_1 {α : Type u} {β : Type v} {𝕜 : Type u_1} [NormedField 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] : IsBoundedSMul (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)

@[implicit_reducible]

instance BoundedContinuousFunction.instPartialOrder {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] : PartialOrder (BoundedContinuousFunction α β)

Equations

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

@[implicit_reducible]

instance BoundedContinuousFunction.instSup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] : Max (BoundedContinuousFunction α β)

Equations

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

@[implicit_reducible]

instance BoundedContinuousFunction.instInf {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] : Min (BoundedContinuousFunction α β)

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_sup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] (f g : BoundedContinuousFunction α β) : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g

@[simp]

theorem BoundedContinuousFunction.coe_inf {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] (f g : BoundedContinuousFunction α β) : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g

@[implicit_reducible]

instance BoundedContinuousFunction.instSemilatticeSup {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] : SemilatticeSup (BoundedContinuousFunction α β)

Equations

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

@[implicit_reducible]

instance BoundedContinuousFunction.instSemilatticeInf {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] : SemilatticeInf (BoundedContinuousFunction α β)

Equations

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

@[implicit_reducible]

instance BoundedContinuousFunction.instLattice {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] : Lattice (BoundedContinuousFunction α β)

Equations

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

@[simp]

theorem BoundedContinuousFunction.coe_abs {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] (f : BoundedContinuousFunction α β) : ⇑|f| = |⇑f|

@[simp]

theorem BoundedContinuousFunction.coe_posPart {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] (f : BoundedContinuousFunction α β) : ⇑f⁺ = (⇑f)⁺

@[simp]

theorem BoundedContinuousFunction.coe_negPart {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] (f : BoundedContinuousFunction α β) : ⇑f⁻ = (⇑f)⁻

instance BoundedContinuousFunction.instHasSolidNorm {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] : HasSolidNorm (BoundedContinuousFunction α β)

instance BoundedContinuousFunction.instIsOrderedAddMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [NormedAddCommGroup β] [Lattice β] [IsOrderedAddMonoid β] : IsOrderedAddMonoid (BoundedContinuousFunction α β)

def BoundedContinuousFunction.nnrealPart {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : BoundedContinuousFunction α NNReal

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

Equations

• f.nnrealPart = BoundedContinuousFunction.comp Real.toNNReal BoundedContinuousFunction.nnrealPart._proof_1 f

@[simp]

theorem BoundedContinuousFunction.nnrealPart_coeFn_eq {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : ⇑f.nnrealPart = Real.toNNReal ∘ ⇑f

def BoundedContinuousFunction.nnnorm {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : BoundedContinuousFunction α NNReal

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

@[simp]

theorem BoundedContinuousFunction.nnnorm_coeFn_eq {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : ⇑f.nnnorm = NNNorm.nnnorm ∘ ⇑f

theorem BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg {α : Type u} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : ⇑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} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : 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.

theorem BoundedContinuousFunction.add_norm_nonneg {α : Type u_1} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : 0 ≤ f + const α ‖f‖

theorem BoundedContinuousFunction.norm_sub_nonneg {α : Type u_1} [TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) : 0 ≤ const α ‖f‖ - f