Compactly supported bounded continuous functions

The two-sided ideal of compactly supported bounded continuous functions taking values in a metric space, with the uniform distance.

noncomputable def compactlySupported (α : Type u_1) (γ : Type u_2) [TopologicalSpace α] [NonUnitalNormedRing γ] : TwoSidedIdeal (BoundedContinuousFunction α γ)

The two-sided ideal of compactly supported functions.

Equations

• compactlySupported α γ = TwoSidedIdeal.mk' {z : BoundedContinuousFunction α γ | HasCompactSupport ⇑z} ⋯ ⋯ ⋯ ⋯ ⋯

def BoundedContinuousFunction.«termC_cb(_,_)» : Lean.ParserDescr

The two-sided ideal of compactly supported functions.

Equations

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

theorem mem_compactlySupported {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] {f : BoundedContinuousFunction α γ} : f ∈ compactlySupported α γ ↔ HasCompactSupport ⇑f

theorem exist_norm_eq {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] [c : Nonempty α] {f : BoundedContinuousFunction α γ} (h : f ∈ compactlySupported α γ) : ∃ (x : α), ‖f x‖ = ‖f‖

theorem norm_lt_iff_of_compactlySupported {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] {f : BoundedContinuousFunction α γ} (h : f ∈ compactlySupported α γ) {M : ℝ} (M0 : 0 < M) : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem norm_lt_iff_of_nonempty_compactlySupported {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] [c : Nonempty α] {f : BoundedContinuousFunction α γ} (h : f ∈ compactlySupported α γ) {M : ℝ} : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

theorem compactlySupported_eq_top_of_isCompact {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] (h : IsCompact Set.univ) : compactlySupported α γ = ⊤

theorem compactlySupported_eq_top {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] [CompactSpace α] : compactlySupported α γ = ⊤

theorem compactlySupported_eq_top_iff {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] [Nontrivial γ] : compactlySupported α γ = ⊤ ↔ IsCompact Set.univ

def ofCompactSupport {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] (g : α → γ) (hg₁ : Continuous g) (hg₂ : HasCompactSupport g) : BoundedContinuousFunction α γ

A compactly supported continuous function is automatically bounded. This constructor gives an object of α →ᵇ γ from g : α → γ and these assumptions.

Equations

• ofCompactSupport g hg₁ hg₂ = { toFun := g, continuous_toFun := hg₁, map_bounded' := ⋯ }

theorem ofCompactSupport_mem {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] (g : α → γ) (hg₁ : Continuous g) (hg₂ : HasCompactSupport g) : ofCompactSupport g hg₁ hg₂ ∈ compactlySupported α γ

@[instance_reducible]

instance instSMulContinuousMapSubtypeBoundedContinuousFunctionMemTwoSidedIdealCompactlySupported {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] : SMul C(α, γ) ↥(compactlySupported α γ)

Equations

• instSMulContinuousMapSubtypeBoundedContinuousFunctionMemTwoSidedIdealCompactlySupported = { smul := fun (g : C(α, γ)) (f : ↥(compactlySupported α γ)) => ⟨ofCompactSupport (⇑g * ⇑↑f) ⋯ ⋯, ⋯⟩ }