Bounded operations

This file introduces type classes for bornologically bounded operations.

In particular, when combined with type classes which guarantee continuity of the same operations, we can equip bounded continuous functions with the corresponding operations.

Main definitions

• BoundedAdd R: a class guaranteeing boundedness of addition.
• BoundedSub R: a class guaranteeing boundedness of subtraction.
• BoundedMul R: a class guaranteeing boundedness of multiplication.

Bounded addition

class BoundedAdd (R : Type u_1) [Bornology R] [Add R] : Prop

A typeclass saying that (p : R × R) ↦ p.1 + p.2 maps any product of bounded sets to a bounded set. This property follows from LipschitzAdd, and thus automatically holds, e.g., for seminormed additive groups.

• isBounded_add : ∀ {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s + t)

theorem BoundedAdd.isBounded_add {R : Type u_1} : ∀ {inst : Bornology R} {inst_1 : Add R} [self : BoundedAdd R] {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s + t)

theorem isBounded_add {R : Type u_1} [Bornology R] [Add R] [BoundedAdd R] {s : Set R} {t : Set R} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) : Bornology.IsBounded (s + t)

theorem add_bounded_of_bounded_of_bounded {R : Type u_1} {X : Type u_2} [PseudoMetricSpace R] [Add R] [BoundedAdd R] {f : X → R} {g : X → R} (f_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C) (g_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C) : ∃ (C : ℝ), ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C

instance instBoundedAddOfLipschitzAdd {R : Type u_1} [PseudoMetricSpace R] [AddMonoid R] [LipschitzAdd R] : BoundedAdd R

Equations

• ⋯ = ⋯

Bounded subtraction

class BoundedSub (R : Type u_1) [Bornology R] [Sub R] : Prop

A typeclass saying that (p : R × R) ↦ p.1 - p.2 maps any product of bounded sets to a bounded set. This property automatically holds for seminormed additive groups, but it also holds, e.g., for ℝ≥0.

• isBounded_sub : ∀ {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t)

theorem BoundedSub.isBounded_sub {R : Type u_1} : ∀ {inst : Bornology R} {inst_1 : Sub R} [self : BoundedSub R] {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t)

theorem isBounded_sub {R : Type u_1} [Bornology R] [Sub R] [BoundedSub R] {s : Set R} {t : Set R} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) : Bornology.IsBounded (s - t)

theorem sub_bounded_of_bounded_of_bounded {R : Type u_1} {X : Type u_2} [PseudoMetricSpace R] [Sub R] [BoundedSub R] {f : X → R} {g : X → R} (f_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C) (g_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C) : ∃ (C : ℝ), ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C

theorem boundedSub_of_lipschitzWith_sub {R : Type u_1} [PseudoMetricSpace R] [Sub R] {K : NNReal} (lip : LipschitzWith K fun (p : R × R) => p.1 - p.2) : BoundedSub R

Bounded multiplication

class BoundedMul (R : Type u_1) [Bornology R] [Mul R] : Prop

A typeclass saying that (p : R × R) ↦ p.1 * p.2 maps any product of bounded sets to a bounded set. This property automatically holds for non-unital seminormed rings, but it also holds, e.g., for ℝ≥0.

• isBounded_mul : ∀ {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s * t)

theorem BoundedMul.isBounded_mul {R : Type u_1} : ∀ {inst : Bornology R} {inst_1 : Mul R} [self : BoundedMul R] {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s * t)

theorem isBounded_mul {R : Type u_1} [Bornology R] [Mul R] [BoundedMul R] {s : Set R} {t : Set R} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) : Bornology.IsBounded (s * t)

theorem isBounded_pow {R : Type u_2} [Bornology R] [Monoid R] [BoundedMul R] {s : Set R} (s_bdd : Bornology.IsBounded s) (n : ℕ) : Bornology.IsBounded ((fun (x : R) => x ^ n) '' s)

theorem mul_bounded_of_bounded_of_bounded {R : Type u_1} {X : Type u_2} [PseudoMetricSpace R] [Mul R] [BoundedMul R] {f : X → R} {g : X → R} (f_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C) (g_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C) : ∃ (C : ℝ), ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C

Bounded operations in seminormed additive commutative groups

theorem SeminormedAddCommGroup.lipschitzWith_sub {R : Type u_1} [SeminormedAddCommGroup R] : LipschitzWith 2 fun (p : R × R) => p.1 - p.2

instance instBoundedSub {R : Type u_1} [SeminormedAddCommGroup R] : BoundedSub R

Equations

• ⋯ = ⋯

Bounded operations in non-unital seminormed rings

instance instBoundedMul {R : Type u_1} [NonUnitalSeminormedRing R] : BoundedMul R

Equations

• ⋯ = ⋯

Bounded operations in ℝ≥0

instance instBoundedSubNNReal : BoundedSub NNReal

Equations

• instBoundedSubNNReal = ⋯

instance instBoundedMulNNReal : BoundedMul NNReal

Equations

• instBoundedMulNNReal = ⋯