Actions

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

Exact transformations of regular shell fields

The actions in this module are the literal transformations used in ABK26: amplitude scaling, real spatial translation, spatial scaling, triadic shell scaling, negation, and signed-permutation conjugation. Each transformation acts on the stored first and second derivatives by the exact chain rule.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.instIsNormableSpaceRealMat (d : ℕ) : IsNormableSpace ℝ (HCPolySupport.Mat d)

Instance caches for the derivative carriers

The derivative carrier Vec d →L[ℝ] Mat d and the Hessian carrier Vec d →L[ℝ] (Vec d →L[ℝ] Mat d) are searched hundreds of times while elaborating this file. Caching the recurring classes once at module level (outside the section, so that every declaration sees them) turns each search into a single step. Every cache below is literally the instance Lean would otherwise rediscover.

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instNormedSpaceDerivCarrier (d : ℕ) : NormedSpace ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instNormedSpaceDerivCarrier d = inferInstance

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instTopDerivCarrier (d : ℕ) : TopologicalSpace (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instTopDerivCarrier d = inferInstance

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instAddCommMonoidDerivCarrier (d : ℕ) : AddCommMonoid (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instAddCommMonoidDerivCarrier d = inferInstance

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instModuleDerivCarrier (d : ℕ) : Module ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instModuleDerivCarrier d = (Algsuperdiff.Frozen.Assumptions.ShellField.instNormedSpaceDerivCarrier d).toModule

@[instance_reducible]

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.instDistribMulActionDerivCarrier (d : ℕ) : DistribMulAction ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

The distributive scalar action on the shell derivative carrier.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instDistribMulActionDerivCarrier d = (Algsuperdiff.Frozen.Assumptions.ShellField.instModuleDerivCarrier d).toDistribMulAction

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instMulActionDerivCarrier (d : ℕ) : MulAction ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instMulActionDerivCarrier d = (Algsuperdiff.Frozen.Assumptions.ShellField.instModuleDerivCarrier d).toMulAction

instance Algsuperdiff.Frozen.Assumptions.ShellField.instSMulCommClassDerivCarrier (d : ℕ) : SMulCommClass ℝ ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

instance Algsuperdiff.Frozen.Assumptions.ShellField.instIsBoundedSMulDerivCarrier (d : ℕ) : IsBoundedSMul ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

instance Algsuperdiff.Frozen.Assumptions.ShellField.instContinuousConstSMulDerivCarrier (d : ℕ) : ContinuousConstSMul ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instNormedAddCommGroupHessianCarrier (d : ℕ) : NormedAddCommGroup (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instNormedAddCommGroupHessianCarrier d = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instNormedSpaceHessianCarrier (d : ℕ) : NormedSpace ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instNormedSpaceHessianCarrier d = ContinuousLinearMap.toNormedSpace

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instTopHessianCarrier (d : ℕ) : TopologicalSpace (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instTopHessianCarrier d = inferInstance

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instAddCommMonoidHessianCarrier (d : ℕ) : AddCommMonoid (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instAddCommMonoidHessianCarrier d = inferInstance

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instModuleHessianCarrier (d : ℕ) : Module ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instModuleHessianCarrier d = (Algsuperdiff.Frozen.Assumptions.ShellField.instNormedSpaceHessianCarrier d).toModule

instance Algsuperdiff.Frozen.Assumptions.ShellField.instSMulCommClassHessianCarrier (d : ℕ) : SMulCommClass ℝ ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

instance Algsuperdiff.Frozen.Assumptions.ShellField.instIsBoundedSMulHessianCarrier (d : ℕ) : IsBoundedSMul ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

instance Algsuperdiff.Frozen.Assumptions.ShellField.instContinuousConstSMulHessianCarrier (d : ℕ) : ContinuousConstSMul ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instSMulHessianEndomorphisms (d : ℕ) : SMul ℝ ((HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instSMulHessianEndomorphisms d = ContinuousLinearMap.instSMul

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.instNormedSpaceEndoCarrier (d : ℕ) : NormedSpace ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d)

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instNormedSpaceEndoCarrier d = inferInstance

theorem Algsuperdiff.Frozen.Assumptions.ShellField.instIsNormableSpaceRealContinuousLinearMapIdVecMat (d : ℕ) : IsNormableSpace ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Amplitude scaling

def Algsuperdiff.Frozen.Assumptions.ShellField.valueScaleMap {d : ℕ} (c : ℝ) : C(HCPolySupport.Mat d, HCPolySupport.Mat d)

Continuous scalar multiplication of matrix values.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.valueScaleMap c = { toFun := fun (M : HCPolySupport.Mat d) => c • M, continuous_toFun := ⋯ }

def Algsuperdiff.Frozen.Assumptions.ShellField.derivScaleMap {d : ℕ} (c : ℝ) : C(HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d, HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Continuous scalar multiplication of first derivatives.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.derivScaleMap c = { toFun := fun (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) => c • D, continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.secondDerivScaleMap {d : ℕ} (c : ℝ) : C(HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d, HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Continuous scalar multiplication of second derivatives.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.secondDerivScaleMap c = { toFun := fun (H : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) => c • H, continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.scaleAmbient {d : ℕ} (c : ℝ) : ShellAmbient d → ShellAmbient d

Scale the values and both stored derivatives of an ambient shell.

Equations

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

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.scale {d : ℕ} (c : ℝ) (j : ShellField d) : ShellField d

Multiply every matrix value by c.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.scale c j = ⟨Algsuperdiff.Frozen.Assumptions.ShellField.scaleAmbient c ↑j, ⋯⟩

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.scale_apply {d : ℕ} (c : ℝ) (j : ShellField d) (x : HCPolySupport.Vec d) : (↑(scale c j)).1 x = c • (↑j).1 x

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.scale_deriv {d : ℕ} (c : ℝ) (j : ShellField d) (x : HCPolySupport.Vec d) : (scale c j).deriv x = c • j.deriv x

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.scale_secondDeriv {d : ℕ} (c : ℝ) (j : ShellField d) (x : HCPolySupport.Vec d) : (scale c j).secondDeriv x = c • j.secondDeriv x

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_scale {d : ℕ} (c : ℝ) : Continuous (scale c)

Real spatial translations

def Algsuperdiff.Frozen.Assumptions.ShellField.translateMap {d : ℕ} (z : HCPolySupport.Vec d) : C(HCPolySupport.Vec d, HCPolySupport.Vec d)

Continuous translation of the spatial argument.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.translateMap z = { toFun := fun (x : HCPolySupport.Vec d) => x + z, continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.translateAmbient {d : ℕ} (z : HCPolySupport.Vec d) : ShellAmbient d → ShellAmbient d

Translate the values and both stored derivatives of an ambient shell.

Equations

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

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.translate {d : ℕ} (z : HCPolySupport.Vec d) (j : ShellField d) : ShellField d

Real translation in the manuscript convention j(x + z).

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.translate z j = ⟨Algsuperdiff.Frozen.Assumptions.ShellField.translateAmbient z ↑j, ⋯⟩

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translate_apply {d : ℕ} (z : HCPolySupport.Vec d) (j : ShellField d) (x : HCPolySupport.Vec d) : (↑(translate z j)).1 x = (↑j).1 (x + z)

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translate_deriv {d : ℕ} (z : HCPolySupport.Vec d) (j : ShellField d) (x : HCPolySupport.Vec d) : (translate z j).deriv x = j.deriv (x + z)

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translate_secondDeriv {d : ℕ} (z : HCPolySupport.Vec d) (j : ShellField d) (x : HCPolySupport.Vec d) : (translate z j).secondDeriv x = j.secondDeriv (x + z)

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translate_zero {d : ℕ} (j : ShellField d) : translate 0 j = j

Translation by the zero vector is the identity on shell fields.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_translate {d : ℕ} (z : HCPolySupport.Vec d) : Continuous (translate z)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_translate {d : ℕ} (z : HCPolySupport.Vec d) : Measurable (translate z)

Spatial scaling and triadic shell scaling

def Algsuperdiff.Frozen.Assumptions.ShellField.spatialMap {d : ℕ} (r : ℝ) : C(HCPolySupport.Vec d, HCPolySupport.Vec d)

Continuous dilation of the spatial argument.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.spatialMap r = { toFun := fun (x : HCPolySupport.Vec d) => r • x, continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.spatialSecondDerivativeMap {d : ℕ} (r : ℝ) : (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d

The second-derivative chain rule for spatial dilation.

Equations

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

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.spatialSecondDerivativeContinuousMap {d : ℕ} (r : ℝ) : C(HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d, HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

The continuous-map bundle for the second-derivative dilation action.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.spatialSecondDerivativeContinuousMap r = { toFun := ⇑(Algsuperdiff.Frozen.Assumptions.ShellField.spatialSecondDerivativeMap r), continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.spatialScaleAmbient {d : ℕ} (r : ℝ) : ShellAmbient d → ShellAmbient d

Dilate a shell's spatial argument with the corresponding derivative factors.

Equations

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

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.spatialScale {d : ℕ} (r : ℝ) (j : ShellField d) : ShellField d

Precompose with x ↦ r • x; the derivative carries the chain-rule factor r.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.spatialScale r j = ⟨Algsuperdiff.Frozen.Assumptions.ShellField.spatialScaleAmbient r ↑j, ⋯⟩

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.spatialScale_apply {d : ℕ} (r : ℝ) (j : ShellField d) (x : HCPolySupport.Vec d) : (↑(spatialScale r j)).1 x = (↑j).1 (r • x)

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.spatialScale_deriv {d : ℕ} (r : ℝ) (j : ShellField d) (x : HCPolySupport.Vec d) : (spatialScale r j).deriv x = r • j.deriv (r • x)

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.spatialScale_secondDeriv {d : ℕ} (r : ℝ) (j : ShellField d) (x : HCPolySupport.Vec d) : (spatialScale r j).secondDeriv x = r ^ 2 • j.secondDeriv (r • x)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_spatialScale {d : ℕ} (r : ℝ) : Continuous (spatialScale r)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_spatialScale {d : ℕ} (r : ℝ) : Measurable (spatialScale r)

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.rescale {d : ℕ} (c r : ℝ) (j : ShellField d) : ShellField d

Combined amplitude and spatial scaling.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.rescale c r j = Algsuperdiff.Frozen.Assumptions.ShellField.scale c (Algsuperdiff.Frozen.Assumptions.ShellField.spatialScale r j)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_rescale {d : ℕ} (c r : ℝ) : Continuous (rescale c r)

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.triadicScale {d : ℕ} (gamma : ℝ) (k : ℤ) (j : ShellField d) : ShellField d

The literal marginal scaling action 3^(γ k) j(3^(-k) ·).

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.triadicScale gamma k j = Algsuperdiff.Frozen.Assumptions.ShellField.rescale (Real.rpow 3 (gamma * ↑k)) (3 ^ k)⁻¹ j

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.triadicScale_apply {d : ℕ} (gamma : ℝ) (k : ℤ) (j : ShellField d) (x : HCPolySupport.Vec d) : (↑(triadicScale gamma k j)).1 x = Real.rpow 3 (gamma * ↑k) • (↑j).1 ((3 ^ k)⁻¹ • x)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_triadicScale {d : ℕ} (gamma : ℝ) (k : ℤ) : Continuous (triadicScale gamma k)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_triadicScale {d : ℕ} (gamma : ℝ) (k : ℤ) : Measurable (triadicScale gamma k)

Negation

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.negate {d : ℕ} (j : ShellField d) : ShellField d

Value and derivative negation, as required by J3.

Equations

• j.negate = Algsuperdiff.Frozen.Assumptions.ShellField.scale (-1) j

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.negate_apply {d : ℕ} (j : ShellField d) (x : HCPolySupport.Vec d) : (↑j.negate).1 x = -(↑j).1 x

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.negate_deriv {d : ℕ} (j : ShellField d) (x : HCPolySupport.Vec d) : j.negate.deriv x = -j.deriv x

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.negate_secondDeriv {d : ℕ} (j : ShellField d) (x : HCPolySupport.Vec d) : j.negate.secondDeriv x = -j.secondDeriv x

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_negate {d : ℕ} : Continuous negate

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_negate {d : ℕ} : Measurable negate

Signed-permutation conjugation

def Algsuperdiff.Frozen.Assumptions.ShellField.matVecContinuousLinearMap {d : ℕ} (R : HCPolySupport.Mat d) : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d

Matrix multiplication bundled as a continuous linear map on vectors.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.matVecContinuousLinearMap R = { toLinearMap := Matrix.toLin' R, cont := ⋯ }

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matVecContinuousLinearMap_apply {d : ℕ} (R : HCPolySupport.Mat d) (x : HCPolySupport.Vec d) : (matVecContinuousLinearMap R) x = HCPolySupport.matVecMul R x

def Algsuperdiff.Frozen.Assumptions.ShellField.conjugateLinearMap {d : ℕ} (R : HCPolySupport.Mat d) : HCPolySupport.Mat d →ₗ[ℝ] HCPolySupport.Mat d

The linear map sending a matrix to its conjugate by R.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.conjugateLinearMap R = { toFun := fun (M : HCPolySupport.Mat d) => HCPolySupport.matTranspose R * M * R, map_add' := ⋯, map_smul' := ⋯ }

def Algsuperdiff.Frozen.Assumptions.ShellField.conjugateContinuousLinearMap {d : ℕ} (R : HCPolySupport.Mat d) : HCPolySupport.Mat d →L[ℝ] HCPolySupport.Mat d

Matrix conjugation bundled as a continuous linear map.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.conjugateContinuousLinearMap R = { toLinearMap := Algsuperdiff.Frozen.Assumptions.ShellField.conjugateLinearMap R, cont := ⋯ }

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.conjugateContinuousLinearMap_apply {d : ℕ} (R M : HCPolySupport.Mat d) : (conjugateContinuousLinearMap R) M = HCPolySupport.matTranspose R * M * R

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.rotateDerivativeMap {d : ℕ} (R : HCPolySupport.Mat d) : (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d

The exact derivative action D ↦ (M ↦ RᵀMR) ∘ D ∘ (v ↦ Rv).

Equations

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

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.rotateDerivativeMap_apply {d : ℕ} (R : HCPolySupport.Mat d) (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) (v : HCPolySupport.Vec d) : ((rotateDerivativeMap R) D) v = HCPolySupport.matTranspose R * D (HCPolySupport.matVecMul R v) * R

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.rotateSecondDerivativeMap {d : ℕ} (R : HCPolySupport.Mat d) : (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d

The exact Hessian action H ↦ (v ↦ w ↦ Rᵀ H (Rv) (Rw) R).

Equations

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

def Algsuperdiff.Frozen.Assumptions.ShellField.rotateValueMap {d : ℕ} (R : HCPolySupport.Mat d) : C(HCPolySupport.Mat d, HCPolySupport.Mat d)

The continuous matrix-value map used by the rotation action.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.rotateValueMap R = { toFun := ⇑(Algsuperdiff.Frozen.Assumptions.ShellField.conjugateContinuousLinearMap R), continuous_toFun := ⋯ }

def Algsuperdiff.Frozen.Assumptions.ShellField.rotateDomainMap {d : ℕ} (R : HCPolySupport.Mat d) : C(HCPolySupport.Vec d, HCPolySupport.Vec d)

The continuous spatial map used by the rotation action.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.rotateDomainMap R = { toFun := ⇑(Algsuperdiff.Frozen.Assumptions.ShellField.matVecContinuousLinearMap R), continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.rotateDerivativeContinuousMap {d : ℕ} (R : HCPolySupport.Mat d) : C(HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d, HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

The continuous first-derivative map used by the rotation action.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.rotateDerivativeContinuousMap R = { toFun := ⇑(Algsuperdiff.Frozen.Assumptions.ShellField.rotateDerivativeMap R), continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.rotateSecondDerivativeContinuousMap {d : ℕ} (R : HCPolySupport.Mat d) : C(HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d, HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

The continuous second-derivative map used by the rotation action.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.rotateSecondDerivativeContinuousMap R = { toFun := ⇑(Algsuperdiff.Frozen.Assumptions.ShellField.rotateSecondDerivativeMap R), continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.rotateAmbient {d : ℕ} (R : HCPolySupport.Mat d) : ShellAmbient d → ShellAmbient d

Rotate a shell's argument, values and stored derivatives together.

Equations

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

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.rotate {d : ℕ} (R : HCPolySupport.Mat d) (_hR : HCPolySupport.IsSignedPermutationMatrix R) (j : ShellField d) : ShellField d

The signed-permutation action j(x) ↦ Rᵀ j(Rx) R.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.rotate R _hR j = ⟨Algsuperdiff.Frozen.Assumptions.ShellField.rotateAmbient R ↑j, ⋯⟩

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.rotate_apply {d : ℕ} (R : HCPolySupport.Mat d) (hR : HCPolySupport.IsSignedPermutationMatrix R) (j : ShellField d) (x : HCPolySupport.Vec d) : (↑(rotate R hR j)).1 x = HCPolySupport.matTranspose R * (↑j).1 (HCPolySupport.matVecMul R x) * R

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_rotate {d : ℕ} (R : HCPolySupport.Mat d) (hR : HCPolySupport.IsSignedPermutationMatrix R) : Continuous (rotate R hR)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_rotate {d : ℕ} (R : HCPolySupport.Mat d) (hR : HCPolySupport.IsSignedPermutationMatrix R) : Measurable (rotate R hR)

Compatibility with CoarseGraining regular-field operations

theorem Algsuperdiff.Frozen.Assumptions.ShellField.forgetShell_translate {d : ℕ} (z : HCPolySupport.Vec d) (j : ShellField d) : (translate z j).forgetShell = HCPolySupport.translateReg z j.forgetShell

theorem Algsuperdiff.Frozen.Assumptions.ShellField.forgetShell_triadicScale {d : ℕ} (gamma : ℝ) (k : ℤ) (j : ShellField d) : (triadicScale gamma k j).forgetShell = Probability.triadicLayerScaleReg gamma k j.forgetShell