Carrier

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

Carriers for the small-contrast Schauder estimate

The analytic core is stated on the explicit Euclidean balls Homogenization.euclideanBall. This choice is substantive: normalized Dirichlet energy of a harmonic function is monotone on concentric Euclidean balls, giving the coefficient 1 in the contraction. Replacing the balls by sup-norm cubes at this point would spend a dimension factor before the perturbative term and destroy the contraction as alpha tends to one.

The eventual coefficient-sigma-field consumer uses scalar coefficients on cubes. It is reached by a separate scalar and ball/cube wrapper; the theorem family here keeps the source's matrix-valued coefficient and ball geometry.

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The normalized Euclidean L² seminorm of a vector field.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On W f = Algsuperdiff.Section4.Support.normalizedL2On W fun (x : HCPolySupport.Vec d) => HCPolySupport.euclideanNorm (f x)

@[reducible, inline]

abbrev Algsuperdiff.StochasticProcess.Common.Regularity.Ported.IsUnitWeaklyHarmonicOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.H1Function W) : Prop

The paper-side unit-coefficient weak harmonicity predicate.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.IsUnitWeaklyHarmonicOn W u = Algsuperdiff.Section4.Support.IsWeaklyHarmonicOn W u

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.CoefficientIdentityDistanceLE {d : ℕ} (W : Set (HCPolySupport.Vec d)) (a : HCPolySupport.CoeffField d) (delta : ℝ) : Prop

The source's L^infinity distance of the coefficient from the identity, written as an a.e. operator-norm bound.

Equations

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

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (p : ℝ) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The real-valued Euclidean L^p size of a vector field.

Equations

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

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.MemVectorLpOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (p : ℝ) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) : Prop

Membership in the vector L^p carrier used by the source.

Equations

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

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (alpha K : ℝ) (v : HCPolySupport.Vec d → ℝ) : Prop

Euclidean Hölder control of a scalar representative.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn W alpha K v = ∀ x ∈ W, ∀ y ∈ W, |v x - v y| ≤ K * HCPolySupport.euclideanNorm (x - y) ^ alpha

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.schauderSourceExponent (d : ℕ) (alpha : ℝ) : ℝ

The source exponent p = d/(1-alpha).

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.schauderSourceExponent d alpha = ↑d / (1 - alpha)

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBall (d : ℕ) : Set (HCPolySupport.Vec d)

The unit Euclidean ball in the project carrier.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBall d = HCPolySupport.euclideanBall 0 1

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastBall (d : ℕ) (r : ℝ) : Set (HCPolySupport.Vec d)

The concentric Euclidean ball of radius r.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastBall d r = HCPolySupport.euclideanBall 0 r

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastDataSize (d : ℕ) (alpha : ℝ) (u : HCPolySupport.H1Function (smallContrastUnitBall d)) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The right-hand side of the Schauder estimate, with the sole (1-alpha)^{-1} price exposed.

Equations

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

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.HasSmallContrastGradientScaleBound {d : ℕ} (alpha K : ℝ) (u : HCPolySupport.H1Function (smallContrastUnitBall d)) : Prop

Scale-invariant gradient control on every concentric sub-ball.

Equations

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

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.SmallContrastSchauderConclusion {d : ℕ} (alpha K : ℝ) (u : HCPolySupport.H1Function (smallContrastUnitBall d)) : Prop

Quotient-safe conclusion of the small-contrast Schauder theorem. The continuous representative is explicit, preventing any pointwise claim about the arbitrary raw representative stored in H1Function.

Equations

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