Primitive cutoff realization

This module contains the primitive cutoff realization and the abstract one-dimensional sharp-cutoff inputs.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakOneDimensionalSharpCutoffStep {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The purely one-dimensional sharp-cutoff approximation step.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakOneDimensionalToDistributionStep {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

Intermediate distributional form of the one-dimensional sharp-cutoff argument.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakOneDimensionalDefectDerivativeIdentity {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

After the one-dimensional radial identity is integrated by parts, the defect pairs to zero against derivatives of compactly supported radial cutoffs.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakOneDimensionalPrimitiveTestFamily {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The primitive-cutoff family needed in the one-dimensional sharp-cutoff argument. It says every smooth compactly supported test function in (0, R0) can be represented, for pairing with the defect, as -phi' for an admissible radial cutoff primitive.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakPrimitiveCutoffRealization (R0 : ℝ) : Prop

A concrete primitive-cutoff realization: every smooth compactly supported test function in (0, R0) is the negative derivative, on (0, R0), of a compactly supported radial cutoff. This predicate contains only the one-dimensional construction, independent of the map Du.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakPrimitiveCutoffRealization (R0 : ℝ) : WeakPrimitiveCutoffRealization R0

Construction of the primitive cutoff using the interval primitive t ↦ ∫ x in t..R0, g x and a smooth bump on the left.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakOneDimensionalPrimitiveTestFamily_of_realization {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hrealize : WeakPrimitiveCutoffRealization R0) : WeakOneDimensionalPrimitiveTestFamily Du R0

The concrete primitive realization discharges the primitive test-family interface used by the distributional sharp-cutoff argument.