LocalContrast

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

Small contrast after freezing a continuous skew field

Subtracting the skew part at a centre and dividing by the scalar symmetric part produces a coefficient equal to the identity at that centre. Continuity makes this coefficient uniformly close to the identity on a sufficiently small ball. On a compact set, the radius can be chosen uniformly.

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff {d : ℕ} (nu : ℝ) (a : HCPolySupport.CoeffField d) (z : HCPolySupport.Vec d) : HCPolySupport.CoeffField d

The coefficient obtained by subtracting the skew part frozen at z and normalizing its scalar symmetric part.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff nu a z y = nu⁻¹ • (a y - (a z - nu • 1))

@[reducible, inline]

noncomputable abbrev Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.matrixToHilbertOperatorLinear {d : ℕ} : HCPolySupport.Mat d →ₗ[ℝ] HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertVec d

Matrix action on the Euclidean realization, as a linear map into bounded operators.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.matrixToHilbertOperatorLinear = Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matrixToHilbertOperatorLinear

@[reducible, inline]

noncomputable abbrev Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.matrixToHilbertOperator {d : ℕ} : HCPolySupport.Mat d →L[ℝ] HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertVec d

Matrix action on the Euclidean realization is continuous in the matrix, by finite-dimensionality.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.matrixToHilbertOperator = Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matrixToHilbertOperator

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedSkewOperator {d : ℕ} (nu : ℝ) (a : HCPolySupport.CoeffField d) : HCPolySupport.Vec d → HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertVec d

The normalized skew coefficient represented as an operator on Euclidean Hilbert space.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedSkewOperator nu a y = Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.matrixToHilbertOperator (nu⁻¹ • (a y - nu • 1))

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.sub_scalar_one_isSkew_of_symmPart_eq {d : ℕ} {nu : ℝ} {A : HCPolySupport.Mat d} (hA : HCPolySupport.symmPart A = nu • 1) : HCPolySupport.matTranspose (A - nu • 1) = -(A - nu • 1)

A matrix whose symmetric part is nu • I differs from that scalar matrix by a skew matrix.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.symmPart_normalizedFrozenCoeff_eq_one {d : ℕ} {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (z y : HCPolySupport.Vec d) : HCPolySupport.symmPart (normalizedFrozenCoeff nu a z y) = 1

The normalized frozen coefficient retains exactly the identity as its symmetric part.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.applyMat_opNorm_le_one_add {d : ℕ} {A : HCPolySupport.Mat d} {delta : ℝ} (hdelta : 0 ≤ delta) (hA : ‖HCPolySupport.HilbertVec.applyMat (A - 1)‖ ≤ delta) : ‖HCPolySupport.HilbertVec.applyMat A‖ ≤ 1 + delta

Operator distance from the identity controls the full operator norm.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isEllipticMatrix_one_sq_one_add_of_symmPart_eq_one {d : ℕ} {A : HCPolySupport.Mat d} {delta : ℝ} (hdelta : 0 ≤ delta) (hsymm : HCPolySupport.symmPart A = 1) (hA : ‖HCPolySupport.HilbertVec.applyMat (A - 1)‖ ≤ delta) : HCPolySupport.IsEllipticMatrix 1 ((1 + delta) ^ 2) A

Exact identity symmetric part plus operator-distance delta derives an ellipticity certificate with explicit constants; no ellipticity hypothesis is assumed.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isEllipticMatrix_normalizedFrozenCoeff {d : ℕ} {nu delta : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) {z y : HCPolySupport.Vec d} (hdelta : 0 ≤ delta) (hy : ‖HCPolySupport.HilbertVec.applyMat (normalizedFrozenCoeff nu a z y - 1)‖ ≤ delta) : HCPolySupport.IsEllipticMatrix 1 ((1 + delta) ^ 2) (normalizedFrozenCoeff nu a z y)

The pointwise ellipticity certificate for the normalized coefficient frozen at z.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.continuousOn_normalizedFrozenCoeff {d : ℕ} {U : Set (HCPolySupport.Vec d)} {nu : ℝ} {a : HCPolySupport.CoeffField d} (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) (z : HCPolySupport.Vec d) : ContinuousOn (normalizedFrozenCoeff nu a z) U

Continuity of the skew part makes every normalized frozen coefficient continuous.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isEllipticFieldOn_normalizedFrozenCoeff {d : ℕ} {U W : Set (HCPolySupport.Vec d)} {nu delta : ℝ} {a : HCPolySupport.CoeffField d} (hW : MeasurableSet W) (hnu : 0 < nu) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) (hWU : W ⊆ U) (z : HCPolySupport.Vec d) (hdelta : 0 ≤ delta) (hbound : ∀ y ∈ W, ‖HCPolySupport.HilbertVec.applyMat (normalizedFrozenCoeff nu a z y - 1)‖ ≤ delta) : HCPolySupport.IsEllipticFieldOn 1 ((1 + delta) ^ 2) W (normalizedFrozenCoeff nu a z)

Ellipticity of the normalized frozen coefficient on a measurable subset of the set carrying the continuity, with the explicit constants 1 and (1 + delta) ^ 2.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_ball_coefficientIdentityDistanceLE_normalizedFrozenCoeff {d : ℕ} {U : Set (HCPolySupport.Vec d)} {nu delta : ℝ} {a : HCPolySupport.CoeffField d} (hU : IsOpen U) (hnu : 0 < nu) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) {z : HCPolySupport.Vec d} (hz : z ∈ U) (hdelta : 0 < delta) : ∃ r > 0, HCPolySupport.euclideanBall z r ⊆ U ∧ Ported.CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall z r) (normalizedFrozenCoeff nu a z) delta ∧ HCPolySupport.IsEllipticFieldOn 1 ((1 + delta) ^ 2) (HCPolySupport.euclideanBall z r) (normalizedFrozenCoeff nu a z)

At every point of an open set, continuity of the skew part gives a ball on which the normalized frozen coefficient is arbitrarily close to the identity in the ruled operator norm.