ShellSum

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

The additive layer on the frozen shell-field carrier

The frozen ShellField carrier of ABK26 bundles a matrix value field with its stored first and second derivatives; up to now the repository only carried the multiplicative actions (amplitude scaling, translation, spatial and triadic scaling, negation, signed-permutation conjugation). This module adds the missing additive operations.

All three defining clauses of the frozen carrier are additive: the two HasFDerivAt clauses by Has.sum, and entrywise antisymmetry linearly. So there is no structural obstruction, and the sum of shell fields carries honest derivative data rather than a re-derived one.

The resulting shellIncrement omega n m is a genuine ShellField whose values are exactly the stream increment k_m - k_n of the manuscript, by shellIncrement_apply_eq_cutoff_sub.

Main definitions

• ShellField.zero, ShellField.add, ShellField.sum: the additive layer.
• shellIncrement: the finite stream increment as a shell field.

Main results

• ShellField.zero_apply, ShellField.add_apply, ShellField.sum_apply and their first- and second-derivative analogues: the defining pointwise characterizations.
• shellIncrement_apply: the increment's values are the proved regular-field increment finiteShellIncrement.
• shellIncrement_apply_eq_cutoff_sub: the increment's values are literally k_m x - k_n x.

References

• ABK26, e.Bosc.def, e.Bosc.decomp.

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

Migration cache (mathlib v4.33.1): ContinuousLinearMap.add on the nested second-derivative fibre needs ContinuousAdd (Vec d →L[ℝ] Mat d) as a hypothesis (the codomain of the outer map). A blind search for that hypothesis tries the IsTopologicalAddGroup.toContinuousAdd route only after first wandering, unsuccessfully, through every Vec d →L[ℝ] Mat d-as-endomorphism-ring candidate (IsSemitopologicalSemiring, IsTopologicalSemiring, down through CStarAlgebra, NormedRing, Field, …), and gives up before ever reaching the right one. Naming the direct term sidesteps that search entirely; it is what the nested-level caches below build on.

@[instance_reducible]

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

Migration cache (mathlib v4.33.1): pin the nested second-derivative fibre's TopologicalSpace/IsTopologicalAddGroup/ContinuousAdd directly via ContinuousLinearMap.topologicalSpace / ContinuousLinearMap.topologicalAddGroup, now that the one-level-down hypothesis (instContinuousAddVecMatCLM above) resolves immediately instead of wandering. An earlier version of this cache instead proved ContinuousAdd at the nested type via a bare inferInstance-built private theorem turned into a local instance; under mathlib v4.33.0 that candidate's explicit (d : ℕ) argument fails to unify with the ambient section d at the actual Continuous.add use sites below (tryResolve reports a stray metavariable), even though the identical goal succeeds when posed in isolation. Building ContinuousAdd directly from a plain (non-local) instance avoids that failure entirely.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instTopologicalSpaceVecVecMatCLM d = ContinuousLinearMap.topologicalSpace

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

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

@[instance_reducible]

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

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.instAddCommGroupVecVecMatCLM d = ContinuousLinearMap.addCommGroup

The zero shell field

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.zero (d : ℕ) : ShellField d

The identically zero shell field, with zero derivative data.

Equations

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

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.zero_apply {d : ℕ} (x : HCPolySupport.Vec d) : (↑(zero d)).1 x = 0

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.zero_deriv {d : ℕ} (x : HCPolySupport.Vec d) : (zero d).deriv x = 0

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.zero_secondDeriv {d : ℕ} (x : HCPolySupport.Vec d) : (zero d).secondDeriv x = 0

Binary sums

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

Continuity of the summed second-derivative field, as a standalone lemma. Ordinary instance search for ContinuousAdd on the nested second-derivative fibre leaves d tied to an unresolved metavariable at every use site below (mathlib v4.33.0), even though the identical goal resolves immediately once posed on its own; supplying instContinuousAddVecVecMatCLM explicitly via @ sidesteps that search rather than relying on it.

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

The pointwise sum of two shell fields, with the summed derivative data.

Equations

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

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.add_apply {d : ℕ} (j k : ShellField d) (x : HCPolySupport.Vec d) : (↑(j.add k)).1 x = (↑j).1 x + (↑k).1 x

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.add_deriv {d : ℕ} (j k : ShellField d) (x : HCPolySupport.Vec d) : (j.add k).deriv x = j.deriv x + k.deriv x

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.add_secondDeriv {d : ℕ} (j k : ShellField d) (x : HCPolySupport.Vec d) : (j.add k).secondDeriv x = j.secondDeriv x + k.secondDeriv x

Finite sums

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_sum_secondDeriv {d : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → ShellField d) : Continuous fun (x : HCPolySupport.Vec d) => ∑ i ∈ s, (f i).secondDeriv x

Continuity of the finite-summed second-derivative field, as a standalone lemma; see continuous_add_secondDeriv for why the needed instances are supplied explicitly via @ rather than left to search.

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.sum {d : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → ShellField d) : ShellField d

The pointwise Finset sum of shell fields, with the summed derivative data. This is the finite-sum carrier required by the literal oscillation event of e.Bosc.def.

Equations

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

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.sum_apply {d : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → ShellField d) (x : HCPolySupport.Vec d) : (↑(sum s f)).1 x = ∑ i ∈ s, (↑(f i)).1 x

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.sum_empty {d : ℕ} {ι : Type u_1} (f : ι → ShellField d) : sum ∅ f = zero d

theorem Algsuperdiff.Frozen.Assumptions.ShellField.sum_cons {d : ℕ} {ι : Type u_1} {a : ι} {s : Finset ι} (ha : a ∉ s) (f : ι → ShellField d) : sum (Finset.cons a s ha) f = (f a).add (sum s f)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translate_sum {d : ℕ} {ι : Type u_1} (z : HCPolySupport.Vec d) (s : Finset ι) (f : ι → ShellField d) : translate z (sum s f) = sum s fun (i : ι) => translate z (f i)

Translation commutes with finite sums of shell fields.

noncomputable def Algsuperdiff.Section3.Provider.Stream.shellIncrement {d : ℕ} (omega : Cutoff.ShellSeq d) (n m : ℤ) : Frozen.Assumptions.ShellField d

The finite stream increment k_m - k_n as a genuine shell field: the literal sum of the shells with indices in (n, m], carrying honest first and second derivative data.

Equations

• Algsuperdiff.Section3.Provider.Stream.shellIncrement omega n m = Algsuperdiff.Frozen.Assumptions.ShellField.sum (Finset.Ioc n m) omega

theorem Algsuperdiff.Section3.Provider.Stream.shellIncrement_apply {d : ℕ} (omega : Cutoff.ShellSeq d) (n m : ℤ) (x : HCPolySupport.Vec d) : (↑(shellIncrement omega n m)).1 x = (Cutoff.finiteShellIncrement omega n m).toFun x

The increment shell field has exactly the values of the proved regular-coefficient-field increment.

theorem Algsuperdiff.Section3.Provider.Stream.shellIncrement_apply_eq_cutoff_sub {d : ℕ} (omega : Cutoff.CutoffSample d) {n m : ℤ} (hnm : n ≤ m) (x : HCPolySupport.Vec d) : (↑(shellIncrement (↑omega) n m)).1 x = (Cutoff.cutoff m omega).toFun x - (Cutoff.cutoff n omega).toFun x

The values of the increment shell field are literally k_m x - k_n x. This is the identification the literal oscillation event e.Bosc.def needs.