Compactly supported smooth test functions

theorem HasCompactSupport.smul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Zero β] [SMulWithZero ℝ β] {c : ℝ} {f : α → β} (hf : HasCompactSupport f) : HasCompactSupport (c • f)

Compactly supported smooth functions supported in an open set U ⊆ ℝᵈ. Elements satisfy: compact support, support contained in U, and C^∞ regularity.

noncomputable def Cc_inftyU (d : ℕ+) (U : Set (Fin ↑d → ℝ)) : Submodule ℝ ((Fin ↑d → ℝ) → ℝ)

Equations

• Cc_inftyU d U = { carrier := {f : (Fin ↑d → ℝ) → ℝ | HasCompactSupport f ∧ tsupport f ⊆ U ∧ ContDiff ℝ (↑⊤) f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[reducible, inline]

noncomputable abbrev Cc_infty (d : ℕ+) : Submodule ℝ ((Fin ↑d → ℝ) → ℝ)

Compactly supported smooth functions on all of ℝᵈ, as the special case U = Set.univ.

Equations

• Cc_infty d = Cc_inftyU d Set.univ

Locally Lp function spaces

noncomputable def Lp_locU (d : ℕ+) (p : ENNReal) (U : Set (Fin ↑d → ℝ)) : Submodule ℝ ((Fin ↑d → ℝ) →ₘ[MeasureTheory.volume] ℝ)

Functions locally in Lᵖ on an open set U ⊆ ℝᵈ: those lying in Lᵖ(C) for every compact C ⊆ U.

Equations

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

@[reducible, inline]

noncomputable abbrev Lp_loc (d : ℕ+) (p : ENNReal) : Submodule ℝ ((Fin ↑d → ℝ) →ₘ[MeasureTheory.volume] ℝ)

Functions locally in Lᵖ on all of ℝᵈ, as the special case U = Set.univ.

Equations

• Lp_loc d p = Lp_locU d p Set.univ

@[simp]

theorem mem_Lp_loc_iff {d : ℕ+} {p : ENNReal} {f : (Fin ↑d → ℝ) →ₘ[MeasureTheory.volume] ℝ} : f ∈ Lp_loc d p ↔ ∀ (C : Set (Fin ↑d → ℝ)), IsCompact C → MeasureTheory.MemLp (↑f) p (MeasureTheory.volume.restrict C)

Membership in Lp_loc unfolds to: MemLp f p (volume.restrict C) for every compact C.

Local integrability

theorem LplocLocallyIntegU (d : ℕ+) (p : ENNReal) (hp : 1 ≤ p) (U : Set (Fin ↑d → ℝ)) (hU : IsOpen U) {f : (Fin ↑d → ℝ) →ₘ[MeasureTheory.volume] ℝ} (hf : f ∈ Lp_locU d p U) : MeasureTheory.LocallyIntegrableOn (↑f) U MeasureTheory.volume

Every function in Lp_locU d p U (with p ≥ 1) is locally integrable on U.

theorem LplocLocallyInteg (d : ℕ+) (p : ENNReal) (hp : 1 ≤ p) {f : (Fin ↑d → ℝ) →ₘ[MeasureTheory.volume] ℝ} (hf : f ∈ Lp_loc d p) : MeasureTheory.LocallyIntegrable (↑f) MeasureTheory.volume

Every function in Lp_loc d p (with p ≥ 1) is locally integrable on ℝᵈ. Derived from LplocLocallyIntegU applied to U = Set.univ.