BoundaryReflectedCoeff

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

Coefficients under one coordinate face reflection

Reflecting a divergence-form coefficient in the hyperplane {y i = c} conjugates the matrix by the coordinate sign flip in direction i. The conjugation fixes the identity and is an isometry for the operator norm, so it preserves exactly the distance-to-identity quantity that the small-contrast estimates consume. The one-face reflected field keeps the original coefficient on the retained half, installs the conjugated pullback on the reflected half, and is the identity on the null interface.

1. Conjugation by a coordinate sign flip

def Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectSign {d : ℕ} (i j : Fin d) : ℝ

The coordinate sign flip attached to the hyperplane with normal i.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectSign i j = if j = i then -1 else 1

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectSign_mul_self {d : ℕ} (i j : Fin d) : faceReflectSign i j * faceReflectSign i j = 1

def Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectMat {d : ℕ} (i : Fin d) (A : HCPolySupport.Mat d) : HCPolySupport.Mat d

Conjugation of a matrix by the coordinate sign flip in direction i.

Equations

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

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectMat_apply {d : ℕ} (i : Fin d) (A : HCPolySupport.Mat d) (j k : Fin d) : faceReflectMat i A j k = faceReflectSign i j * (faceReflectSign i k * A j k)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectMat_one {d : ℕ} (i : Fin d) : faceReflectMat i 1 = 1

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectMat_sub {d : ℕ} (i : Fin d) (A B : HCPolySupport.Mat d) : faceReflectMat i (A - B) = faceReflectMat i A - faceReflectMat i B

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.coordReflectionLinear_involutive_local {d : ℕ} (i : Fin d) (v : HCPolySupport.Vec d) : (HCPolySupport.coordReflectionLinear i) ((HCPolySupport.coordReflectionLinear i) v) = v

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.vecDot_coordReflectionLinear_both {d : ℕ} (i : Fin d) (v w : HCPolySupport.Vec d) : HCPolySupport.vecDot ((HCPolySupport.coordReflectionLinear i) v) ((HCPolySupport.coordReflectionLinear i) w) = HCPolySupport.vecDot v w

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.matVecMul_faceReflectMat {d : ℕ} (i : Fin d) (A : HCPolySupport.Mat d) (v : HCPolySupport.Vec d) : HCPolySupport.matVecMul (faceReflectMat i A) v = (HCPolySupport.coordReflectionLinear i) (HCPolySupport.matVecMul A ((HCPolySupport.coordReflectionLinear i) v))

The conjugated matrix acts on the reflected vector by reflecting the original action.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.matVecMul_faceReflectMat_coordReflectionLinear {d : ℕ} (i : Fin d) (A : HCPolySupport.Mat d) (v : HCPolySupport.Vec d) : HCPolySupport.matVecMul (faceReflectMat i A) ((HCPolySupport.coordReflectionLinear i) v) = (HCPolySupport.coordReflectionLinear i) (HCPolySupport.matVecMul A v)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.norm_ofVec_coordReflectionLinear {d : ℕ} (i : Fin d) (v : HCPolySupport.Vec d) : ‖HCPolySupport.HilbertVec.ofVec ((HCPolySupport.coordReflectionLinear i) v)‖ = ‖HCPolySupport.HilbertVec.ofVec v‖

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.norm_applyMat_faceReflectMat {d : ℕ} (i : Fin d) (A : HCPolySupport.Mat d) : ‖HCPolySupport.HilbertVec.applyMat (faceReflectMat i A)‖ = ‖HCPolySupport.HilbertVec.applyMat A‖

Conjugation by a coordinate sign flip is an isometry of the operator norm.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.norm_applyMat_faceReflectMat_sub_one {d : ℕ} (i : Fin d) (A : HCPolySupport.Mat d) : ‖HCPolySupport.HilbertVec.applyMat (faceReflectMat i A - 1)‖ = ‖HCPolySupport.HilbertVec.applyMat (A - 1)‖

Conjugation preserves the distance to the identity.

2. The one-face reflected coefficient field

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectedCoeff {d : ℕ} (c : ℝ) (i : Fin d) (sigma : ℝ) (a : HCPolySupport.CoeffField d) : HCPolySupport.CoeffField d

The one-face reflected coefficient in the hyperplane {y i = c}: the original field on the sigma-side, the conjugated pullback on the other side, and the identity on the interface.

Equations

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

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectedCoeff_of_pos {d : ℕ} {c : ℝ} {i : Fin d} {sigma : ℝ} (a : HCPolySupport.CoeffField d) {y : HCPolySupport.Vec d} (hy : 0 < sigma * (c - y i)) : faceReflectedCoeff c i sigma a y = a y

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectedCoeff_of_neg {d : ℕ} {c : ℝ} {i : Fin d} {sigma : ℝ} (a : HCPolySupport.CoeffField d) {y : HCPolySupport.Vec d} (hy : 0 < sigma * (y i - c)) : faceReflectedCoeff c i sigma a y = faceReflectMat i (a (HCPolySupport.coordFaceReflection c i y))

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.coordFaceReflection_coord {d : ℕ} (c : ℝ) (i : Fin d) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection c i y i = 2 * c - y i

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectedCoeff_eq_on_faceHalf {d : ℕ} {c : ℝ} {i : Fin d} {sigma : ℝ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {y : HCPolySupport.Vec d} (hy : y ∈ Section4.Provider.ExcessDecay.faceHalf U i c sigma) : faceReflectedCoeff c i sigma a y = a y

Off the interface hyperplane, membership in the retained half is decided by the sign condition.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.faceReflectedCoeff_eq_reflected {d : ℕ} {c : ℝ} {i : Fin d} {sigma : ℝ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {y : HCPolySupport.Vec d} (hy : y ∈ U) (hynot : y ∉ Section4.Provider.ExcessDecay.faceHalf U i c sigma) (hne : y i ≠ c) (hsigma : sigma ≠ 0) : faceReflectedCoeff c i sigma a y = faceReflectMat i (a (HCPolySupport.coordFaceReflection c i y))

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.measurable_faceReflectedCoeff {d : ℕ} {c : ℝ} {i : Fin d} {sigma : ℝ} {a : HCPolySupport.CoeffField d} (ha : Measurable a) : Measurable (faceReflectedCoeff c i sigma a)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.coefficientIdentityDistanceLE_faceReflectedCoeff {d : ℕ} {c : ℝ} {i : Fin d} {sigma : ℝ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {delta : ℝ} (hsigma : sigma ≠ 0) (hUopen : IsOpen U) (hUsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection c i y ∈ U ↔ y ∈ U) (ha : Ported.CoefficientIdentityDistanceLE (Section4.Provider.ExcessDecay.faceHalf U i c sigma) a delta) : Ported.CoefficientIdentityDistanceLE U (faceReflectedCoeff c i sigma a) delta

The reflected field inherits the small-contrast bound of the original field on the retained half.