small inputs of the no-selection argument

• TwoDiffusivityContract: classical solutions with the same drift and two diffusivities stay close in L² on [0,1];
• CosineDatumContract: facts about the cosine data c cos (2π n x₀);
• VelGradContract: the gradient of the stream-sequence drift is O(ε_m^{β-2});
• A0CoreContract: the ingredient-level form of the main theorem for the limit field of one stream sequence.

def AVenhance.Infra.FullTheorem.TwoDiffusivityContract : Prop

Same drift, two diffusivities: the L² distance on [0,1] is |κ-κ'|/(2√(κκ')) ‖θ₀‖.

Equations

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

def AVenhance.Infra.FullTheorem.CosineDatumContract : Prop

Facts about the cosine data.

Equations

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

def AVenhance.Infra.FullTheorem.VelGradContract (β C₀ : ℝ) : Prop

Gradient bound for the drift of the stream sequence.

Equations

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

def AVenhance.Infra.FullTheorem.A0CoreContract (β C₀ : ℝ) : Prop

The main theorem at ingredient level, for the limit field of one stream sequence (for 6/5 ≤ β).

Equations

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