OneStepCornerTransportHarmonic

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

Classical harmonicity under a coordinate negation

The analytic half of the lower/mixed-face transport of the §4.3 boundary branch. The proved odd-class apparatus is stated at upper met faces; the domain cube □_m is origin-symmetric, so negating one coordinate carries a lower-face-met window to an upper-face-met one. For that transport to be usable the classical harmonicity of the competitor has to travel with it, which is what this module supplies.

The mechanism

Precomposition with a linear isometry equivalence L of the Euclidean carrier commutes with the Laplacian:

  Δ (f ∘ L) = (Δ f) ∘ L ,

with no differentiability hypothesis. Indeed the iterated derivative of a right-composition with a continuous linear equivalence is unconditional (ContinuousLinearEquiv.iterated at s = univ), and Δ may be read in *any* orthonormal basis (laplacian_eq_iterated), in particular in the image L ∘ b of a fixed one. Harmonicity then transports because ContDiffAt composes and the vanishing germ of Δ f pulls back along the continuous L.

Coordinate negation is such an L: it is LinearIsometryEquiv.piLpCongrRight 2 of the per-coordinate negations, and it matches CoarseGraining's coordFaceReflection (0 : ℝ) i across the carrier identification toEuc.

1. The Laplacian under a linear isometry of the domain

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.laplacian_comp_linearIsometryEquiv {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℝ) (L : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)) (z : EuclideanSpace ℝ (Fin d)) : Laplacian.laplacian (f ∘ ⇑L) z = Laplacian.laplacian f (L z)

The Laplacian commutes with precomposition by a linear isometry equivalence. Unconditional: no differentiability of f is needed.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicAt_comp_linearIsometryEquiv {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (L : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)) {z : EuclideanSpace ℝ (Fin d)} (h : InnerProductSpace.HarmonicAt f (L z)) : InnerProductSpace.HarmonicAt (f ∘ ⇑L) z

Harmonicity travels with a linear isometry of the domain.

2. Coordinate negation as a linear isometry

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.negCoordLIE {d : ℕ} (i : Fin d) : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)

Negation of the i-th coordinate of the Euclidean carrier, as a linear isometry equivalence.

Equations

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

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.negCoordLIE_apply {d : ℕ} (i : Fin d) (z : EuclideanSpace ℝ (Fin d)) (l : Fin d) : ((negCoordLIE i) z).ofLp l = if l = i then -z.ofLp l else z.ofLp l

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc_symm_negCoordLIE {d : ℕ} (i : Fin d) (z : EuclideanSpace ℝ (Fin d)) : toEuc.symm ((negCoordLIE i) z) = HCPolySupport.coordFaceReflection 0 i (toEuc.symm z)

The Euclidean coordinate negation is CoarseGraining's coordFaceReflection (0: ℝ) i read across the carrier identification.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc_negCoordLIE {d : ℕ} (i : Fin d) (y : HCPolySupport.Vec d) : (negCoordLIE i) (toEuc y) = toEuc (HCPolySupport.coordFaceReflection 0 i y)

3. The transport of HarmonicOnNhd

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_comp_coordFaceReflection_zero {d : ℕ} {S : Set (HCPolySupport.Vec d)} {V : HCPolySupport.Vec d → ℝ} (i : Fin d) (hV : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' S)) : InnerProductSpace.HarmonicOnNhd ((fun (y : HCPolySupport.Vec d) => V (HCPolySupport.coordFaceReflection 0 i y)) ∘ ⇑toEuc.symm) (⇑toEuc '' HCPolySupport.coordFaceReflection 0 i ⁻¹' S)

Classical harmonicity under a coordinate negation. If V is harmonic on (the Euclidean image of) S, then V ∘ σ_i is harmonic on the Euclidean image of σ_i ⁻¹' S.