J2Observable

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

The exact J2 shell observable

This module defines the three quantitative norms in ABK26 assumption J2 on the literal open cube cu₀ = (-1/2, 1/2)^d and proves that their weighted sum is Borel measurable on the compact-open ShellField carrier.

The matrix value norm is Homogenization.Book.Ch02.matrixOperatorNorm. Derivative inputs use Homogenization.Book.Ch02.vecNorm. The stored first and second derivatives remain bundled with the frozen carrier's elementwise matrix norm; their exact Euclidean induced norms are explicit scalar suprema, so no alternative matrix-norm instance leaks into the carrier. Every supremum includes zero explicitly.

@[reducible, inline]

abbrev Algsuperdiff.Frozen.Assumptions.ShellField.MatrixDerivative (d : ℕ) : Type

The stored first-derivative type of a shell field. Its bundle uses the elementwise matrix norm fixed by the frozen carrier; exact Euclidean sizes are measured separately by matrixDerivativeNorm.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.MatrixDerivative d = (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

@[reducible, inline]

abbrev Algsuperdiff.Frozen.Assumptions.ShellField.EuclideanUnitVector (d : ℕ) : Type

The closed Euclidean unit ball used to index induced derivative norms.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.EuclideanUnitVector d = { v : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm v ≤ 1 }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNormValue {d : ℕ} (D : MatrixDerivative d) : Option (EuclideanUnitVector d) → ℝ

Values used for the exact Euclidean induced norm. The none branch records zero explicitly, including in dimension zero.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNormValue D none = 0
• Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNormValue D (some v) = HCPolySupport.Book.Ch02.matrixOperatorNorm (D ↑v)

def Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNormValueSet {d : ℕ} (D : MatrixDerivative d) : Set ℝ

The range of first-derivative norm samples, including the zero sample.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNormValueSet D = Set.range (Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNormValue D)

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm {d : ℕ} (D : MatrixDerivative d) : ℝ

Euclidean-vector to Euclidean-matrix induced norm, evaluated on the carrier's actual elementwise-norm continuous-linear-map bundle.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm D = sSup (Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNormValueSet D)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.norm_vec_le_vecNorm {d : ℕ} (v : HCPolySupport.Vec d) : ‖v‖ ≤ HCPolySupport.Book.Ch02.vecNorm v

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm_nonneg {d : ℕ} (D : MatrixDerivative d) : 0 ≤ matrixDerivativeNorm D

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixOperatorNorm_apply_le_matrixDerivativeNorm {d : ℕ} (D : MatrixDerivative d) (v : HCPolySupport.Vec d) (hv : HCPolySupport.Book.Ch02.vecNorm v ≤ 1) : HCPolySupport.Book.Ch02.matrixOperatorNorm (D v) ≤ matrixDerivativeNorm D

The exact induced derivative norm controls every matrix value on the vecNorm unit ball.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm_le_sq_mul_norm {d : ℕ} (D : MatrixDerivative d) : matrixDerivativeNorm D ≤ ↑d ^ 2 * ‖D‖

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm_add_le {d : ℕ} (D E : MatrixDerivative d) : matrixDerivativeNorm (D + E) ≤ matrixDerivativeNorm D + matrixDerivativeNorm E

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm_neg {d : ℕ} (D : MatrixDerivative d) : matrixDerivativeNorm (-D) = matrixDerivativeNorm D

theorem Algsuperdiff.Frozen.Assumptions.ShellField.norm_matrixDerivativeNorm_sub_le_sq_mul_norm {d : ℕ} (D E : MatrixDerivative d) : ‖matrixDerivativeNorm D - matrixDerivativeNorm E‖ ≤ ↑d ^ 2 * ‖D - E‖

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm_lipschitz {d : ℕ} : LipschitzWith (↑d ^ 2).toNNReal matrixDerivativeNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm_continuous {d : ℕ} : Continuous matrixDerivativeNorm

@[reducible, inline]

abbrev Algsuperdiff.Frozen.Assumptions.ShellField.MatrixSecondDerivative (d : ℕ) : Type

The stored second-derivative type of a shell field. It is a linear map in the first derivative direction with values in MatrixDerivative d.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.MatrixSecondDerivative d = (HCPolySupport.Vec d →L[ℝ] Algsuperdiff.Frozen.Assumptions.ShellField.MatrixDerivative d)

@[instance_reducible]

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

Migration cache (mathlib v4.33.1): blind instance search no longer reaches the ContinuousLinearMap normed-group instance on the nested Vec d →L[ℝ] MatrixDerivative d carrier, so ‖H‖, H.le_opNorm and dist_eq_norm below would fail; name the direct term once here.

Equations

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

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNormValue {d : ℕ} (H : MatrixSecondDerivative d) : Option (EuclideanUnitVector d) → ℝ

Values used for the exact twice-induced Euclidean norm. The none branch records zero explicitly, including in dimension zero.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNormValue H none = 0
• Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNormValue H (some v) = Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm (H ↑v)

def Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNormValueSet {d : ℕ} (H : MatrixSecondDerivative d) : Set ℝ

The range of second-derivative norm samples, including the zero sample.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNormValueSet H = Set.range (Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNormValue H)

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm {d : ℕ} (H : MatrixSecondDerivative d) : ℝ

Exact twice-induced norm of a stored second derivative: first take the exact induced norm of the resulting matrix derivative, then the supremum over the first vecNorm unit ball.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm H = sSup (Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNormValueSet H)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm_nonneg {d : ℕ} (H : MatrixSecondDerivative d) : 0 ≤ matrixSecondDerivativeNorm H

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm_apply_le_matrixSecondDerivativeNorm {d : ℕ} (H : MatrixSecondDerivative d) (u : HCPolySupport.Vec d) (hu : HCPolySupport.Book.Ch02.vecNorm u ≤ 1) : matrixDerivativeNorm (H u) ≤ matrixSecondDerivativeNorm H

The exact twice-induced norm controls the inner derivative norm for every first input in the vecNorm unit ball.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm_add_le {d : ℕ} (H K : MatrixSecondDerivative d) : matrixSecondDerivativeNorm (H + K) ≤ matrixSecondDerivativeNorm H + matrixSecondDerivativeNorm K

theorem Algsuperdiff.Frozen.Assumptions.ShellField.norm_matrixSecondDerivativeNorm_sub_le_sq_mul_norm {d : ℕ} (H K : MatrixSecondDerivative d) : ‖matrixSecondDerivativeNorm H - matrixSecondDerivativeNorm K‖ ≤ ↑d ^ 2 * ‖H - K‖

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm_lipschitz {d : ℕ} : LipschitzWith (↑d ^ 2).toNNReal matrixSecondDerivativeNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm_continuous {d : ℕ} : Continuous matrixSecondDerivativeNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm_le_iff {d : ℕ} (H : MatrixSecondDerivative d) (C : ℝ) : matrixSecondDerivativeNorm H ≤ C ↔ 0 ≤ C ∧ ∀ (u : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm u ≤ 1 → matrixDerivativeNorm (H u) ≤ C

Sharp characterization of the exact twice-induced norm.

@[reducible, inline]

abbrev Algsuperdiff.Frozen.Assumptions.ShellField.UnitOpenCubePoint (d : ℕ) : Type

Points of the literal open manuscript cube cu₀ = (-1/2, 1/2)^d.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.UnitOpenCubePoint d = { x : HCPolySupport.Vec d // x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0) }

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeValueAtIndex {d : ℕ} (j : ShellField d) : Option (UnitOpenCubePoint d) → ℝ

Matrix-value norm samples on the open unit cube, with zero at none.

Equations

• j.unitCubeValueAtIndex none = 0
• j.unitCubeValueAtIndex (some x_1) = HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 ↑x_1)

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeDerivAtIndex {d : ℕ} (j : ShellField d) : Option (UnitOpenCubePoint d) → ℝ

First-derivative norm samples on the open unit cube, with zero at none.

Equations

• j.unitCubeDerivAtIndex none = 0
• j.unitCubeDerivAtIndex (some x_1) = Algsuperdiff.Frozen.Assumptions.ShellField.matrixDerivativeNorm (j.deriv ↑x_1)

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeSecondDerivAtIndex {d : ℕ} (j : ShellField d) : Option (UnitOpenCubePoint d) → ℝ

Second-derivative norm samples on the open unit cube, with zero at none.

Equations

• j.unitCubeSecondDerivAtIndex none = 0
• j.unitCubeSecondDerivAtIndex (some x_1) = Algsuperdiff.Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm (j.secondDeriv ↑x_1)

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

Exact Euclidean matrix-operator L∞ norm of the shell values on the literal open unit cube. The defining range includes zero explicitly.

Equations

• j.unitCubeValueNorm = sSup (Set.range j.unitCubeValueAtIndex)

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

Exact induced vecNorm → matrixOperatorNorm L∞ norm of the stored first derivative on the literal open unit cube.

Equations

• j.unitCubeDerivNorm = sSup (Set.range j.unitCubeDerivAtIndex)

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

Exact twice-induced vecNorm → vecNorm → matrixOperatorNorm L∞ norm of the stored second derivative on the literal open unit cube.

Equations

• j.unitCubeSecondDerivNorm = sSup (Set.range j.unitCubeSecondDerivAtIndex)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeValueNorm_nonneg {d : ℕ} (j : ShellField d) : 0 ≤ j.unitCubeValueNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixOperatorNorm_apply_le_unitCubeValueNorm {d : ℕ} (j : ShellField d) (x : UnitOpenCubePoint d) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 ↑x) ≤ j.unitCubeValueNorm

The unit-cube value control bounds the matrix operator norm at every point of the literal open unit cube.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.continuous_matrixOperatorNorm {d : ℕ} : Continuous HCPolySupport.Book.Ch02.matrixOperatorNorm

Continuity of the exact Euclidean matrix-operator norm used by the J2 observable.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeDerivNorm_nonneg {d : ℕ} (j : ShellField d) : 0 ≤ j.unitCubeDerivNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeSecondDerivNorm_nonneg {d : ℕ} (j : ShellField d) : 0 ≤ j.unitCubeSecondDerivNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeSecondDerivNorm_le_iff {d : ℕ} (j : ShellField d) (C : ℝ) : j.unitCubeSecondDerivNorm ≤ C ↔ 0 ≤ C ∧ ∀ (x : UnitOpenCubePoint d), matrixSecondDerivativeNorm (j.secondDeriv ↑x) ≤ C

Sharp characterization: the open-cube second-derivative norm is the least nonnegative constant controlling the exact twice-induced norm at every point of the literal open cube.

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.j2Observable (d : ℕ) (j : ShellField d) : ℝ

The literal weighted observable in the manuscript's J2 tail bound: ‖j₀‖∞ + √d ‖∇j₀‖∞ + d ‖∇²j₀‖∞, all on the open cube cu₀.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.j2Observable d j = j.unitCubeValueNorm + √↑d * j.unitCubeDerivNorm + ↑d * j.unitCubeSecondDerivNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.j2Observable_nonneg (d : ℕ) (j : ShellField d) : 0 ≤ j2Observable d j

The J2 observable is nonnegative.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeValueNorm_lowerSemicontinuous {d : ℕ} : LowerSemicontinuous unitCubeValueNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeDerivNorm_lowerSemicontinuous {d : ℕ} : LowerSemicontinuous unitCubeDerivNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeSecondDerivNorm_lowerSemicontinuous {d : ℕ} : LowerSemicontinuous unitCubeSecondDerivNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeValueNorm_measurable {d : ℕ} : Measurable unitCubeValueNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeDerivNorm_measurable {d : ℕ} : Measurable unitCubeDerivNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.unitCubeSecondDerivNorm_measurable {d : ℕ} : Measurable unitCubeSecondDerivNorm

theorem Algsuperdiff.Frozen.Assumptions.ShellField.j2Observable_measurable (d : ℕ) : Measurable (j2Observable d)