TranslationAction

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

Real translation action on shell-value paths

The manuscript uses the real translation convention (τ_z f)(x) = f(x + z). This module proves that it is a jointly continuous additive action on the compact-open carrier C(Vec d, Mat d), the carrier of the stationary zero-shell law used by J4.

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.valuePathMeasurableSpace (d : ℕ) : MeasurableSpace C(HCPolySupport.Vec d, HCPolySupport.Mat d)

The Borel sigma-field of the compact-open shell-value path space.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.valuePathMeasurableSpace d = borel C(HCPolySupport.Vec d, HCPolySupport.Mat d)

instance Algsuperdiff.Frozen.Assumptions.ShellField.valuePathBorelSpace (d : ℕ) : BorelSpace C(HCPolySupport.Vec d, HCPolySupport.Mat d)

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

The value component of a regular shell field, viewed as a compact-open continuous matrix-valued path. This is the canonical carrier of the zero-shell law used in J1 and J4.

Equations

• j.valuePath = (↑j).1

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_valuePath {d : ℕ} : Continuous valuePath

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_valuePath {d : ℕ} : Measurable valuePath

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

The continuous map x ↦ x + z used to express a real translation.

Equations

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

Value-path translations

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

Real translation of a shell-value path in the manuscript convention f(x) ↦ f(x + z).

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.translateValue z f = f.comp (Algsuperdiff.Frozen.Assumptions.ShellField.translationMap z)

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translateValue_apply {d : ℕ} (z : HCPolySupport.Vec d) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) (x : HCPolySupport.Vec d) : (translateValue z f) x = f (x + z)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_translateValue_joint {d : ℕ} : Continuous fun (q : HCPolySupport.Vec d × C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => translateValue q.1 q.2

Joint continuity in the shift and the compact-open value path.

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translateValue_zero {d : ℕ} (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : translateValue 0 f = f

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translateValue_add {d : ℕ} (z w : HCPolySupport.Vec d) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : translateValue (z + w) f = translateValue z (translateValue w f)

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.valuePathAddAction {d : ℕ} : AddAction (HCPolySupport.Vec d) C(HCPolySupport.Vec d, HCPolySupport.Mat d)

The real translations of value paths, in the manuscript convention z +ᵥ f = f(· + z).

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.valuePathAddAction = { vadd := Algsuperdiff.Frozen.Assumptions.ShellField.translateValue, add_vadd := ⋯, zero_vadd := ⋯ }

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.vadd_apply {d : ℕ} (z : HCPolySupport.Vec d) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) (x : HCPolySupport.Vec d) : (z +ᵥ f) x = f (x + z)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_vadd_joint {d : ℕ} : Continuous fun (q : HCPolySupport.Vec d × C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => q.1 +ᵥ q.2

The joint continuity statement expressed through the additive action.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_vadd_const {d : ℕ} (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : Continuous fun (z : HCPolySupport.Vec d) => z +ᵥ f

The orbit of a fixed value path is continuous in the translation vector.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_const_vadd {d : ℕ} (z : HCPolySupport.Vec d) : Continuous fun (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => z +ᵥ f

Translation by a fixed vector is continuous on value paths.

instance Algsuperdiff.Frozen.Assumptions.ShellField.valuePathContinuousVAdd {d : ℕ} : ContinuousVAdd (HCPolySupport.Vec d) C(HCPolySupport.Vec d, HCPolySupport.Mat d)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_vadd_joint {d : ℕ} : Measurable (Function.uncurry fun (x1 : HCPolySupport.Vec d) (x2 : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => x1 +ᵥ x2)

Joint measurability of the real translation action.

instance Algsuperdiff.Frozen.Assumptions.ShellField.valuePathMeasurableVAdd {d : ℕ} : MeasurableVAdd (HCPolySupport.Vec d) C(HCPolySupport.Vec d, HCPolySupport.Mat d)

instance Algsuperdiff.Frozen.Assumptions.ShellField.valuePathMeasurableVAdd₂ {d : ℕ} : MeasurableVAdd₂ (HCPolySupport.Vec d) C(HCPolySupport.Vec d, HCPolySupport.Mat d)

Projection compatibility

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.valuePath_translate {d : ℕ} (z : HCPolySupport.Vec d) (j : ShellField d) : (translate z j).valuePath = translateValue z j.valuePath

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

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.valuePath_negate {d : ℕ} (j : ShellField d) : j.negate.valuePath = -j.valuePath

Local sigma-fields on the canonical value-path carrier