OneStepSchauderKernel

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

The native unit-mass radial mollifier

The interior Schauder estimate is proved by the reproducing-convolution route: a harmonic function reproduces itself against any unit-mass radial kernel, and derivatives are then moved onto the kernel, where they are bounded by an explicit dimensional constant. This module builds that kernel:

• radialProfile — the scalar profile s ↦ smoothTransition (1 - s);
• radialKernelAux d — x ↦ radialProfile ‖x‖², smooth, nonnegative, radial, supported in the closed unit ball, positive at the origin;
• radialKernel d — the same divided by its (strictly positive) mass, so ∫ radialKernel d = 1;
• radialKernelScaled d ε — the ε-dilate z ↦ (ε^d)⁻¹ · radialKernel d (ε⁻¹ • z), supported in closedBall 0 ε, again of unit mass.

The scalar radial profile

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialProfile (s : ℝ) : ℝ

The scalar radial profile s ↦ smoothTransition (1 - s): C^∞, nonnegative, = 1 for s ≤ 0, positive for s < 1, and = 0 for 1 ≤ s. Composed with the squared norm it yields a smooth radial bump supported in the unit ball. (Port of K radialSqProfile, mathlib-native.)

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialProfile s = (1 - s).smoothTransition

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialProfile_contDiff {n : ℕ∞} : ContDiff ℝ (↑n) radialProfile

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialProfile_nonneg (s : ℝ) : 0 ≤ radialProfile s

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialProfile_eq_zero_of_one_le {s : ℝ} (hs : 1 ≤ s) : radialProfile s = 0

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialProfile_zero : radialProfile 0 = 1

The un-normalized radial kernel

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux (d : ℕ) : EuclideanSpace ℝ (Fin d) → ℝ

The un-normalized native radial mollifier on EuclideanSpace ℝ (Fin d): x ↦ radialProfile (‖x‖²). Smooth, nonnegative, radial, supported in the closed unit ball, and positive at the origin.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux d x = Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialProfile (‖x‖ ^ 2)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_contDiff (d : ℕ) {n : ℕ∞} : ContDiff ℝ (↑n) (radialKernelAux d)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_nonneg (d : ℕ) (x : EuclideanSpace ℝ (Fin d)) : 0 ≤ radialKernelAux d x

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_radial (d : ℕ) {x y : EuclideanSpace ℝ (Fin d)} (h : ‖x‖ = ‖y‖) : radialKernelAux d x = radialKernelAux d y

Radiality. The un-normalized kernel depends on x only through ‖x‖.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_eq_zero_of_one_le_norm (d : ℕ) {x : EuclideanSpace ℝ (Fin d)} (hx : 1 ≤ ‖x‖) : radialKernelAux d x = 0

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_zero (d : ℕ) : radialKernelAux d 0 = 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.support_radialKernelAux_subset (d : ℕ) : Function.support (radialKernelAux d) ⊆ Metric.closedBall 0 1

The support of the un-normalized kernel is contained in the closed unit ball.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.tsupport_radialKernelAux_subset (d : ℕ) : tsupport (radialKernelAux d) ⊆ Metric.closedBall 0 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_hasCompactSupport (d : ℕ) : HasCompactSupport (radialKernelAux d)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_continuous (d : ℕ) : Continuous (radialKernelAux d)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_integral_pos (d : ℕ) : 0 < ∫ (x : EuclideanSpace ℝ (Fin d)), radialKernelAux d x

Strictly positive mass. The un-normalized kernel has a strictly positive integral (it is a nonnegative continuous compactly-supported function, positive at the origin).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelAux_integral_ne_zero (d : ℕ) : ∫ (x : EuclideanSpace ℝ (Fin d)), radialKernelAux d x ≠ 0

The unit-mass radial kernel

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernel (d : ℕ) : EuclideanSpace ℝ (Fin d) → ℝ

The unit-mass native radial mollifier on EuclideanSpace ℝ (Fin d): the un-normalized kernel divided by its (strictly positive) total mass. Smooth, nonnegative, radial, supported in the closed unit ball, and of total mass 1. (Native port of K normalizedRadialSqProfile.)

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernel_contDiff (d : ℕ) {n : ℕ∞} : ContDiff ℝ (↑n) (radialKernel d)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernel_radial (d : ℕ) {x y : EuclideanSpace ℝ (Fin d)} (h : ‖x‖ = ‖y‖) : radialKernel d x = radialKernel d y

Radiality. The unit-mass kernel depends on x only through ‖x‖.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernel_eq_zero_of_one_le_norm (d : ℕ) {x : EuclideanSpace ℝ (Fin d)} (hx : 1 ≤ ‖x‖) : radialKernel d x = 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.support_radialKernel_subset (d : ℕ) : Function.support (radialKernel d) ⊆ Metric.closedBall 0 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.tsupport_radialKernel_subset (d : ℕ) : tsupport (radialKernel d) ⊆ Metric.closedBall 0 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernel_hasCompactSupport (d : ℕ) : HasCompactSupport (radialKernel d)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernel_integral_eq_one (d : ℕ) : ∫ (x : EuclideanSpace ℝ (Fin d)), radialKernel d x = 1

Unit mass. The normalized kernel integrates to 1.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled (d : ℕ) (ε : ℝ) : EuclideanSpace ℝ (Fin d) → ℝ

The ε-scaled native radial mollifier: K_ε(z) = ε⁻ᵈ · radialKernel d (ε⁻¹ • z).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled d ε z = (ε ^ d)⁻¹ * Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernel d (ε⁻¹ • z)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled_apply (d : ℕ) (ε : ℝ) (z : EuclideanSpace ℝ (Fin d)) : radialKernelScaled d ε z = (ε ^ d)⁻¹ * radialKernel d (ε⁻¹ • z)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled_contDiff (d : ℕ) {ε : ℝ} {n : ℕ∞} : ContDiff ℝ (↑n) (radialKernelScaled d ε)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled_radial (d : ℕ) {ε : ℝ} {a b : EuclideanSpace ℝ (Fin d)} (h : ‖a‖ = ‖b‖) : radialKernelScaled d ε a = radialKernelScaled d ε b

Radiality. The scaled kernel depends on z only through ‖z‖.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled_eq_zero_of_le_norm (d : ℕ) {ε : ℝ} (hε : 0 < ε) {z : EuclideanSpace ℝ (Fin d)} (hz : ε ≤ ‖z‖) : radialKernelScaled d ε z = 0

The scaled kernel vanishes outside the open ball of radius ε.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.support_radialKernelScaled_subset (d : ℕ) {ε : ℝ} (hε : 0 < ε) : Function.support (radialKernelScaled d ε) ⊆ Metric.closedBall 0 ε

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.tsupport_radialKernelScaled_subset (d : ℕ) {ε : ℝ} (hε : 0 < ε) : tsupport (radialKernelScaled d ε) ⊆ Metric.closedBall 0 ε

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled_hasCompactSupport (d : ℕ) {ε : ℝ} (hε : 0 < ε) : HasCompactSupport (radialKernelScaled d ε)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled_continuous (d : ℕ) {ε : ℝ} : Continuous (radialKernelScaled d ε)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.radialKernelScaled_integral_eq_one (d : ℕ) {ε : ℝ} (hε : 0 < ε) : ∫ (z : EuclideanSpace ℝ (Fin d)), radialKernelScaled d ε z = 1

Unit mass. The ε-rescaling preserves total mass: ∫ K_ε = 1. The dilation Jacobian ε⁻ᵈ exactly cancels the εᵈ from the change of variables z ↦ ε⁻¹ • z.