CompactSupportDenseCore

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Compactly supported functions as a dense core of C₀

This file realizes compactly supported bounded continuous functions as a norm-preserving continuous linear subspace of C₀. On a locally compact regular space, its inclusion has dense range. The density proof cuts a function off by a compactly supported Urysohn function.

This is purely functional-analytic infrastructure. In applications to divergence-form regularity, a separate support-preserving smoothing argument can refine this continuous core to a smooth compactly supported core.

@[reducible, inline]

noncomputable abbrev DivergenceFormProcess.FunctionalAnalysis.CompactSupportCore (X : Type u_2) [TopologicalSpace X] : TwoSidedIdeal (BoundedContinuousFunction X ℝ)

Compactly supported bounded continuous real-valued functions, equipped with the uniform norm.

Equations

• DivergenceFormProcess.FunctionalAnalysis.CompactSupportCore X = compactlySupported X ℝ

def DivergenceFormProcess.FunctionalAnalysis.compactSupportCoreToC0Linear {X : Type u_1} [TopologicalSpace X] : ↥(CompactSupportCore X) →ₗ[ℝ] ZeroAtInftyContinuousMap X ℝ

The linear inclusion of the compact-support core into continuous functions vanishing at infinity.

Equations

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

theorem DivergenceFormProcess.FunctionalAnalysis.norm_compactSupportCoreToC0Linear {X : Type u_1} [TopologicalSpace X] (f : ↥(CompactSupportCore X)) : ‖compactSupportCoreToC0Linear f‖ = ‖f‖

The compact-support inclusion preserves the uniform norm.

noncomputable def DivergenceFormProcess.FunctionalAnalysis.compactSupportCoreToC0 {X : Type u_1} [TopologicalSpace X] : ↥(CompactSupportCore X) →L[ℝ] ZeroAtInftyContinuousMap X ℝ

The norm-preserving continuous linear inclusion of the compact-support core into C₀.

Equations

• DivergenceFormProcess.FunctionalAnalysis.compactSupportCoreToC0 = DivergenceFormProcess.FunctionalAnalysis.compactSupportCoreToC0Linear.mkContinuous 1 ⋯

theorem DivergenceFormProcess.FunctionalAnalysis.denseRange_compactSupportCoreToC0 {X : Type u_1} [TopologicalSpace X] [R1Space X] [LocallyCompactSpace X] : DenseRange ⇑compactSupportCoreToC0

Compactly supported bounded continuous functions are uniformly dense in C₀ on a locally compact regular space.