BoundaryFreezingRadius

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

Freezing at a point of a closed axis cube

At any point of the closed cube — a face, an edge or a corner included — the coefficient frozen and normalized at that point equals the identity there. Continuity on the closed cube therefore produces a radius on which it stays uniformly close to the identity, and the finitely many coordinate gaps produce a radius on which no unincident face is met. Taking the smaller of the two radii gives the scale at which the boundary sector is the intersection of a ball with the cube and the frozen coefficient has small contrast.

A coefficient whose symmetric part is the scalar matrix nu * I is elliptic with lower constant nu, and its upper constant is controlled by any bound on the operator norm of its skew part; on a compact set continuity supplies such a bound. So continuity alone, with no restriction on the size of the skew part, produces a full ellipticity certificate.

1. Continuity of the distance to the identity

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.continuous_norm_applyMat_sub_one {d : ℕ} : Continuous fun (A : HCPolySupport.Mat d) => ‖HCPolySupport.HilbertVec.applyMat (A - 1)‖

The operator distance of a matrix from the identity is continuous.

2. Measurability of the frozen coefficient

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.measurable_normalizedFrozenCoeff {d : ℕ} {nu : ℝ} {a : HCPolySupport.CoeffField d} (ha : Measurable a) (x₀ : HCPolySupport.Vec d) : Measurable (normalizedFrozenCoeff nu a x₀)

3. The freezing radius at a point of the closed cube

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff_self {d : ℕ} {nu : ℝ} (hnu : 0 < nu) (a : HCPolySupport.CoeffField d) (x₀ : HCPolySupport.Vec d) : normalizedFrozenCoeff nu a x₀ x₀ = 1

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_boundary_freezing_radius {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) {x : HCPolySupport.Vec d | MemAxisCubeClosure z L x}) {x₀ : HCPolySupport.Vec d} (hx₀ : MemAxisCubeClosure z L x₀) {delta : ℝ} (hdelta : 0 < delta) : ∃ R > 0, AxisCubeFaceClearance z L R x₀ ∧ ∀ y ∈ HCPolySupport.euclideanBall x₀ R, MemAxisCubeClosure z L y → ‖HCPolySupport.HilbertVec.applyMat (normalizedFrozenCoeff nu a x₀ y - 1)‖ ≤ delta

A radius at a point of the closed cube on which no unincident face is met and the frozen normalized coefficient is delta-close to the identity.

4. Ellipticity from a scalar symmetric part and a bounded skew part

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isEllipticMatrix_of_symmPart_eq_of_opNorm_le {d : ℕ} {nu M : ℝ} (hnu : 0 < nu) {A : HCPolySupport.Mat d} (hsymm : HCPolySupport.symmPart A = nu • 1) (hM : ‖HCPolySupport.HilbertVec.applyMat (A - nu • 1)‖ ≤ M) : HCPolySupport.IsEllipticMatrix nu ((nu ^ 2 + M ^ 2) / nu) A

Ellipticity of a matrix with scalar symmetric part. If the symmetric part of A is nu * I then the quadratic form of A is exactly nu |xi|^2, and the skew part contributes nothing to it, so an operator-norm bound M on the skew part gives the flux inequality with upper constant (nu ^ 2 + M ^ 2) / nu. No smallness of the skew part is required.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isEllipticFieldOn_of_symmPart_eq_of_continuousOn {d : ℕ} {W K : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (hWK : W ⊆ K) {nu M : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) K) (hM : ∀ y ∈ K, ‖HCPolySupport.HilbertVec.applyMat (a y - nu • 1)‖ ≤ M) : HCPolySupport.IsEllipticFieldOn nu ((nu ^ 2 + M ^ 2) / nu) W a

Ellipticity of a continuous coefficient field with scalar symmetric part. A bound M on the operator norm of the skew part over a set K carrying the continuity gives the ellipticity certificate on every measurable subset W of K, with constants nu and (nu ^ 2 + M ^ 2) / nu.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_isEllipticFieldOn_of_symmPart_eq_of_isCompact {d : ℕ} {W K : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (hK : IsCompact K) (hWK : W ⊆ K) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) K) : ∃ (Lam : ℝ), HCPolySupport.IsEllipticFieldOn nu Lam W a

Ellipticity from compactness and continuity alone. On a compact set the skew part is bounded, so a coefficient with scalar symmetric part and continuous skew part of arbitrary size is elliptic on every measurable subset, with constants that compactness supplies.