Ellipticity

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

Local ellipticity of the genuine cutoff

The lower-infinite cutoff is controlled on each origin cube by the same summable local-control series that licenses its construction. In particular, the nonsymmetric coefficient field has lower ellipticity nu, but its upper ellipticity constant also records the realised skew part. It is never set to nu merely because the symmetric part is nu I.

theorem Algsuperdiff.Section3.Cutoff.abs_cutoff_entry_le_cutoffLocalControl {d : ℕ} (ell m : ℤ) (omega : CutoffSample d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) (i j : Fin d) : |(cutoff m omega).toFun x i j| ≤ cutoffLocalControl ell m omega

Every entry of the genuine cutoff is bounded by its realised local control on the matching open origin cube.

theorem Algsuperdiff.Section3.Cutoff.abs_coefficientCutoff_entry_le {d : ℕ} (nu : ℝ) (hnu : 0 ≤ nu) (ell m : ℤ) (omega : CutoffSample d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) (i j : Fin d) : |(coefficientCutoff nu m omega).toFun x i j| ≤ nu + cutoffLocalControl ell m omega

A pointwise entry bound for the actual coefficient cutoff on an origin cube. The nu term is the diagonal constant field; the second term is the realised lower-cutoff control.

A finite-dimensional ellipticity producer

This is deliberately local proof infrastructure. It transports the exact quadratic-form identity from Limit.lean plus a literal entry bound into CoarseGraining's nonsymmetric IsEllipticMatrix predicate.

theorem Algsuperdiff.Section3.Cutoff.isEllipticMatrix_of_symmPart_and_entry_bound {d : ℕ} {A : HCPolySupport.Mat d} {nu C : ℝ} (hnu : 0 < nu) (hsymm : HCPolySupport.symmPart A = nu • 1) (hentry : ∀ (i j : Fin d), |A i j| ≤ C) : HCPolySupport.IsEllipticMatrix nu ((↑d * ↑d * C ^ 2 + nu ^ 2) / nu) A

theorem Algsuperdiff.Section3.Cutoff.isEllipticFieldOn_coefficientCutoff_of_entry_bound {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (C : ℝ) (hentry : ∀ x ∈ U, ∀ (i j : Fin d), |(coefficientCutoff M.nu m omega).toFun x i j| ≤ C) : HCPolySupport.IsEllipticFieldOn M.nu ((↑d * ↑d * C ^ 2 + M.nu ^ 2) / M.nu) U (coefficientCutoff M.nu m omega).toFun

A local entry bound gives an honest nonsymmetric ellipticity certificate for the actual coefficient field on any measurable region.