CoefficientBounds

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

Pointwise consequences of small contrast

The source informally replaces ||a-Id|| <= delta by Id <= a. The latter does not follow. The correct consequence is coercivity at 1-delta; combined with delta < 1/2, it gives the same factor 2 in the harmonic-comparison estimate printed in the proof.

@[instance_reducible]

instance Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matMeasurableSpace {d : ℕ} : MeasurableSpace (HCPolySupport.Mat d)

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matMeasurableSpace = Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matMeasurableSpace._aux_1

instance Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matBorelSpace {d : ℕ} : BorelSpace (HCPolySupport.Mat d)

@[instance_reducible]

noncomputable instance Algsuperdiff.StochasticProcess.Common.Regularity.Ported.hilbertVecOperatorMeasurableSpace {d : ℕ} : MeasurableSpace (HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertVec d)

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.hilbertVecOperatorMeasurableSpace = borel (HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertVec d)

instance Algsuperdiff.StochasticProcess.Common.Regularity.Ported.hilbertVecOperatorBorelSpace {d : ℕ} : BorelSpace (HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertVec d)

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

The linear map taking a matrix to its Euclidean Hilbert-space operator.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matrixToHilbertOperatorLinear = { toFun := HCPolySupport.HilbertVec.applyMat, map_add' := ⋯, map_smul' := ⋯ }

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

The continuous linear map taking a matrix to its Euclidean Hilbert-space operator.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matrixToHilbertOperator = { toLinearMap := Algsuperdiff.StochasticProcess.Common.Regularity.Ported.matrixToHilbertOperatorLinear, cont := ⋯ }

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.memVectorL2_coefficientSubIdentity_mul {d : ℕ} {W : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {H : HCPolySupport.Vec d → HCPolySupport.Vec d} {delta : ℝ} (hmeas : AEMeasurable a (MeasureTheory.volume.restrict W)) (ha : CoefficientIdentityDistanceLE W a delta) (hH : HCPolySupport.MemVectorL2 W H) : HCPolySupport.MemVectorL2 W fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a x - 1) (H x)

A measurable coefficient satisfying the a.e. small-contrast bound maps an L² vector field through a - Id into L²; no pointwise ellipticity certificate is needed.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.memVectorL2_coefficient_mul {d : ℕ} {W : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {H : HCPolySupport.Vec d → HCPolySupport.Vec d} {delta : ℝ} (hmeas : AEMeasurable a (MeasureTheory.volume.restrict W)) (ha : CoefficientIdentityDistanceLE W a delta) (hH : HCPolySupport.MemVectorL2 W H) : HCPolySupport.MemVectorL2 W fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a x) (H x)

The same hypotheses give L² integrability of the full coefficient action.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vecNormSq_matVecMul_le_applyMat_opNorm_sq_mul {d : ℕ} (A : HCPolySupport.Mat d) (v : HCPolySupport.Vec d) : HCPolySupport.vecNormSq (HCPolySupport.matVecMul A v) ≤ ‖HCPolySupport.HilbertVec.applyMat A‖ ^ 2 * HCPolySupport.vecNormSq v

The ruled Hilbert-space operator norm controls the squared Euclidean magnitude of matrix action.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.abs_vecDot_coefficient_sub_identity_le {d : ℕ} {A : HCPolySupport.Mat d} {delta : ℝ} (hA : ‖HCPolySupport.HilbertVec.applyMat (A - 1)‖ ≤ delta) (v : HCPolySupport.Vec d) : |HCPolySupport.vecDot v (HCPolySupport.matVecMul (A - 1) v)| ≤ delta * HCPolySupport.vecNormSq v

Operator-norm closeness controls the perturbative quadratic form.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.one_sub_mul_vecNormSq_le_vecDot_coefficient {d : ℕ} {A : HCPolySupport.Mat d} {delta : ℝ} (hA : ‖HCPolySupport.HilbertVec.applyMat (A - 1)‖ ≤ delta) (v : HCPolySupport.Vec d) : (1 - delta) * HCPolySupport.vecNormSq v ≤ HCPolySupport.vecDot v (HCPolySupport.matVecMul A v)

The honest lower ellipticity bound supplied by small contrast.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.half_mul_vecNormSq_le_vecDot_coefficient_of_smallContrast {d : ℕ} {A : HCPolySupport.Mat d} {alpha : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) (hA : ‖HCPolySupport.HilbertVec.applyMat (A - 1)‖ ≤ smallContrastThreshold d alpha) (v : HCPolySupport.Vec d) : 1 / 2 * HCPolySupport.vecNormSq v ≤ HCPolySupport.vecDot v (HCPolySupport.matVecMul A v)

The printed smallness assumption supplies the honest half-coercivity used in the corrected energy test.