Basic

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

Basic A for regular shell fields

This module equips the exact frozen shell-field carrier with its compact-open topology and Borel measurable space. It also exposes the value and first- and second-derivative data, derives the exact C^2 regularity, proves that values determine a shell, and gives the measurable forgetful map into CoarseGraining's RegCoeffField.

@[reducible, inline]

abbrev Algsuperdiff.Frozen.Assumptions.ShellAmbient (d : ℕ) : Type

The ambient compact-open triple underlying the frozen shell carrier.

Equations

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

@[instance_reducible]

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

Equations

• Algsuperdiff.Frozen.Assumptions.shellFieldNormedAddCommGroup d = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

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

Equations

• Algsuperdiff.Frozen.Assumptions.shellFieldNormedSpace d = ContinuousLinearMap.toNormedSpace

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.shellFieldTopologicalSpace (d : ℕ) : TopologicalSpace (ShellField d)

Equations

• Algsuperdiff.Frozen.Assumptions.shellFieldTopologicalSpace d = Algsuperdiff.Frozen.Assumptions.shellFieldCompactOpenTopology d

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.shellFieldMeasurableSpace (d : ℕ) : MeasurableSpace (ShellField d)

Equations

• Algsuperdiff.Frozen.Assumptions.shellFieldMeasurableSpace d = Algsuperdiff.Frozen.Assumptions.shellFieldBorelMeasurableSpace d

instance Algsuperdiff.Frozen.Assumptions.shellFieldBorelSpace (d : ℕ) : BorelSpace (ShellField d)

@[instance_reducible]

instance Algsuperdiff.Frozen.Assumptions.ShellField.instCoeFunShellField {d : ℕ} : CoeFun (ShellField d) fun (x : ShellField d) => HCPolySupport.Vec d → HCPolySupport.Mat d

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instCoeFunShellField = { coe := fun (j : Algsuperdiff.Frozen.Assumptions.ShellField d) => ⇑(↑j).1 }

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

The continuous first derivative stored in the exact frozen carrier.

Equations

• j.deriv = (↑j).2.1

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

The continuous second derivative stored in the exact frozen carrier.

Equations

• j.secondDeriv = (↑j).2.2

theorem Algsuperdiff.Frozen.Assumptions.ShellField.hasFDerivAt {d : ℕ} (j : ShellField d) (x : HCPolySupport.Vec d) : HasFDerivAt (⇑(↑j).1) (j.deriv x) x

theorem Algsuperdiff.Frozen.Assumptions.ShellField.deriv_hasFDerivAt {d : ℕ} (j : ShellField d) (x : HCPolySupport.Vec d) : HasFDerivAt (⇑j.deriv) (j.secondDeriv x) x

theorem Algsuperdiff.Frozen.Assumptions.ShellField.contDiff_deriv {d : ℕ} (j : ShellField d) : ContDiff ℝ 1 ⇑j.deriv

The stored first derivative is continuously differentiable.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.contDiff_two {d : ℕ} (j : ShellField d) : ContDiff ℝ 2 ⇑(↑j).1

A frozen shell field is genuinely C^2, with no added regularity hypothesis.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.skew_entry {d : ℕ} (j : ShellField d) (x : HCPolySupport.Vec d) (i k : Fin d) : (↑j).1 x i k = -(↑j).1 x k i

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

theorem Algsuperdiff.Frozen.Assumptions.ShellField.deriv_unique {d : ℕ} (j : ShellField d) {x : HCPolySupport.Vec d} {D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d} (hD : HasFDerivAt (⇑(↑j).1) D x) : D = j.deriv x

A derivative compatible with the same value field is unique.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.secondDeriv_unique {d : ℕ} (j : ShellField d) {x : HCPolySupport.Vec d} {D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d} (hD : HasFDerivAt (⇑j.deriv) D x) : D = j.secondDeriv x

A second derivative compatible with the stored first derivative is unique.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.ext {d : ℕ} {j k : ShellField d} (h : ∀ (x : HCPolySupport.Vec d), (↑j).1 x = (↑k).1 x) : j = k

Shell values determine the entire regular-version datum, including both stored derivatives.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.ext_iff {d : ℕ} {j k : ShellField d} : j = k ↔ ∀ (x : HCPolySupport.Vec d), (↑j).1 x = (↑k).1 x

def Algsuperdiff.Frozen.Assumptions.ShellField.forgetShell {d : ℕ} (j : ShellField d) : HCPolySupport.RegCoeffField d

Forget the shell packaging while retaining the literal matrix values.

Equations

• j.forgetShell = { toFun := ⇑(↑j).1, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.forgetShell_apply {d : ℕ} (j : ShellField d) (x : HCPolySupport.Vec d) : j.forgetShell.toFun x = (↑j).1 x

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_eval {d : ℕ} (x : HCPolySupport.Vec d) : Continuous fun (j : ShellField d) => (↑j).1 x

Evaluation at a fixed point is continuous in the compact-open topology.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_eval {d : ℕ} (x : HCPolySupport.Vec d) : Measurable fun (j : ShellField d) => (↑j).1 x

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_eval_entry {d : ℕ} (x : HCPolySupport.Vec d) (i k : Fin d) : Measurable fun (j : ShellField d) => (↑j).1 x i k

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_eval_deriv {d : ℕ} (x : HCPolySupport.Vec d) : Continuous fun (j : ShellField d) => j.deriv x

Evaluation of the stored first derivative at a fixed point is continuous in the compact-open topology.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_eval_secondDeriv {d : ℕ} (x : HCPolySupport.Vec d) : Continuous fun (j : ShellField d) => j.secondDeriv x

Evaluation of the stored second derivative at a fixed point is continuous in the compact-open topology.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_forgetShell {d : ℕ} : Measurable forgetShell

The forgetful map is measurable for CoarseGraining's full regular-field sigma-field, including the compactly supported integral generators.