OneStepSchauderLapTransfer

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

The Laplacian dictionary and the mollification calculus (Weyl, part 1)

The competitor of the Schauder gradient-Hölder estimate is produced by ResidualCorrectorExistence as an H¹ function satisfying the variational condition Support.IsWeaklyHarmonicOn; the interior Schauder estimate consumes the classical object, Mathlib's InnerProductSpace.HarmonicOnNhd. Bridging the two is Weyl's lemma. This module carries the two calculus halves of that bridge:

• the Laplacian dictionary — Δ (v ∘ toEuc.symm) (toEuc x) = euclideanCoordLaplacian v x for v ∈ C², and its packaging into HarmonicOnNhd on an open set / a sup-metric ball, through the orthonormal-basis formula for Δ;
• the mollification calculus — the coordinate Laplacian commutes with left convolution by a smooth compactly supported kernel, is invariant under the point reflection y ↦ A - y, and scales quadratically under an affine homothety y ↦ a • y + b (this last is what converts CoarseGraining's convex smoothing operator back into a plain convolution Laplacian).

Basis vectors and fderiv across the identification

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.fderiv_comp_toEuc_symm {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (z : EuclideanSpace ℝ (Fin d)) : fderiv ℝ (v ∘ ⇑toEuc.symm) z = fderiv ℝ v (toEuc.symm z) ∘SL ↑toEuc.symm

Chain rule for the pullback along toEuc.symm. No differentiability hypothesis is needed: toEuc.symm is a continuous linear equivalence, and right-composition with such an equivalence commutes with fderiv unconditionally.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.fderiv_comp_toEuc_symm_single {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (z : EuclideanSpace ℝ (Fin d)) (i : Fin d) : (fderiv ℝ (v ∘ ⇑toEuc.symm) z) (EuclideanSpace.single i 1) = HCPolySupport.euclideanCoordDeriv i v (toEuc.symm z)

The derivative of the pullback in a standard basis direction is the CoarseGraining coordinate derivative.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.fderiv_comp_toEuc_symm_single_eq {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (i : Fin d) : (fun (z : EuclideanSpace ℝ (Fin d)) => (fderiv ℝ (v ∘ ⇑toEuc.symm) z) (EuclideanSpace.single i 1)) = HCPolySupport.euclideanCoordDeriv i v ∘ ⇑toEuc.symm

As a function identity: the standard-direction derivative of the pullback is the pullback of the CoarseGraining coordinate derivative.

Second derivatives

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.dirDeriv2_single_comp_toEuc_symm {d : ℕ} (v : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) (i : Fin d) : dirDeriv2 (EuclideanSpace.single i 1) (v ∘ ⇑toEuc.symm) (toEuc x) = HCPolySupport.euclideanCoordSecondDeriv i i v x

The second directional derivative of the pullback, in a standard basis direction, is the CoarseGraining coordinate second derivative. Unconditional.

The Laplacian dictionary

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.laplacian_comp_toEuc_symm_apply {d : ℕ} {v : HCPolySupport.Vec d → ℝ} (hv : ContDiff ℝ 2 v) (x : HCPolySupport.Vec d) : Laplacian.laplacian (v ∘ ⇑toEuc.symm) (toEuc x) = HCPolySupport.euclideanCoordLaplacian v x

The Laplacian dictionary. For a C² function v on the CoarseGraining coordinate carrier, mathlib's coordinate-free Laplacian of the pullback v ∘ toEuc.symm at toEuc x is the CoarseGraining coordinate Laplacian of v at x.

Proof: read Δ in the orthonormal basis EuclideanSpace.basisFun, convert each diagonal iterated derivative into a second directional derivative (iteratedFDeriv_two_eq_dirDeriv2), and transfer each along toEuc (dirDeriv2_single_comp_toEuc_symm).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanCoordLaplacian_eq_laplacian_comp_toEuc_symm {d : ℕ} {v : HCPolySupport.Vec d → ℝ} (hv : ContDiff ℝ 2 v) (z : EuclideanSpace ℝ (Fin d)) : HCPolySupport.euclideanCoordLaplacian v (toEuc.symm z) = Laplacian.laplacian (v ∘ ⇑toEuc.symm) z

Pointwise form: the coordinate Laplacian of v at toEuc.symm z.

Packaging as mathlib harmonicity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_comp_toEuc_symm {d : ℕ} {v : HCPolySupport.Vec d → ℝ} (hv : ContDiff ℝ 2 v) {S : Set (HCPolySupport.Vec d)} (hS : IsOpen S) (hzero : ∀ y ∈ S, HCPolySupport.euclideanCoordLaplacian v y = 0) : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) (⇑toEuc.symm ⁻¹' S)

From a vanishing coordinate Laplacian to mathlib harmonicity. If v is C² on the CoarseGraining coordinate carrier and its coordinate Laplacian vanishes on an open set S, then the pullback v ∘ toEuc.symm is HarmonicOnNhd on the preimage of S.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_ball_comp_toEuc_symm {d : ℕ} {v : HCPolySupport.Vec d → ℝ} (hv : ContDiff ℝ 2 v) {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hzero : ∀ y ∈ Metric.ball x r, HCPolySupport.euclideanCoordLaplacian v y = 0) : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) (Metric.ball (toEuc x) r)

Sup-metric ball version. A vanishing coordinate Laplacian on the product-metric ball Metric.ball x r ⊆ Vec d gives mathlib harmonicity of the pullback on the Euclidean ball Metric.ball (toEuc x) r ⊆ EuclideanSpace ℝ (Fin d) of the same radius.

There is no loss of radius: the L² norm dominates the sup norm on the same data, so the Euclidean ball is contained in the preimage of the sup ball (Homogenization.euclideanBall_subset_metricBall via the ball dictionary mem_euclideanBall_toEuc_iff).

Convolution commutes with coordinate differentiation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanCoordDeriv_convolution_left {d : ℕ} {K g : HCPolySupport.Vec d → ℝ} (hK_supp : HasCompactSupport K) (hK : ContDiff ℝ (↑⊤) K) (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (i : Fin d) : HCPolySupport.euclideanCoordDeriv i (MeasureTheory.convolution K g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) = MeasureTheory.convolution (HCPolySupport.euclideanCoordDeriv i K) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

Coordinate differentiation commutes with left convolution by a smooth compactly supported kernel.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanCoordSecondDeriv_convolution_left {d : ℕ} {K g : HCPolySupport.Vec d → ℝ} (hK_supp : HasCompactSupport K) (hK : ContDiff ℝ (↑⊤) K) (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (i j : Fin d) : HCPolySupport.euclideanCoordSecondDeriv i j (MeasureTheory.convolution K g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) = MeasureTheory.convolution (HCPolySupport.euclideanCoordSecondDeriv i j K) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

Coordinate second derivatives commute with left convolution by a smooth compact kernel.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanCoordLaplacian_convolution_left {d : ℕ} {K g : HCPolySupport.Vec d → ℝ} (hK_supp : HasCompactSupport K) (hK : ContDiff ℝ (↑⊤) K) (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) : HCPolySupport.euclideanCoordLaplacian (MeasureTheory.convolution K g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) = MeasureTheory.convolution (HCPolySupport.euclideanCoordLaplacian K) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

The coordinate Laplacian commutes with left convolution by a smooth compactly supported kernel: Δ (K ⋆ g) = (Δ K) ⋆ g.

Behaviour under the point reflection y ↦ A - y

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanCoordDeriv_comp_const_sub {d : ℕ} {K : HCPolySupport.Vec d → ℝ} (hK : ContDiff ℝ (↑⊤) K) (A : HCPolySupport.Vec d) (i : Fin d) (x : HCPolySupport.Vec d) : HCPolySupport.euclideanCoordDeriv i (fun (y : HCPolySupport.Vec d) => K (A - y)) x = -HCPolySupport.euclideanCoordDeriv i K (A - x)

Coordinate derivative after precomposition with the point reflection y ↦ A - y.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanCoordLaplacian_comp_const_sub {d : ℕ} {K : HCPolySupport.Vec d → ℝ} (hK : ContDiff ℝ (↑⊤) K) (A x : HCPolySupport.Vec d) : HCPolySupport.euclideanCoordLaplacian (fun (y : HCPolySupport.Vec d) => K (A - y)) x = HCPolySupport.euclideanCoordLaplacian K (A - x)

The coordinate Laplacian is invariant under the point reflection y ↦ A - y.

Behaviour under the affine homothety y ↦ a • y + b

Reflecting a convolution integral onto the domain

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.integral_mul_indicator_const_sub_eq_setIntegral {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (A : HCPolySupport.Vec d) (f u : HCPolySupport.Vec d → ℝ) : ∫ (t : HCPolySupport.Vec d), f t * U.indicator u (A - t) = ∫ (y : HCPolySupport.Vec d) in U, u y * f (A - y)

Change of variables by the point reflection t ↦ A - t, converting a global indicator integral into a set integral over U. This is what turns the value of a convolution against the zero-extension 1_U u into a test-function pairing on U.