Inputs for the uniform-regularity part (ii) of the combined main theorem

• ForcedEnergySupContract: the sup-in-time L² form of the stream-difference estimate (hypotheses of Section5.RelativeError.stream_difference_energy);
• HeatApproxH1Contract: Section5.analytic_approximation with the extra conjunct that the heat approximant does not increase the H¹ seminorm;
• WeakDifferenceContract: the L² contraction of the difference of two weak solutions with the same divergence-free drift.

def AVenhance.Infra.FullTheorem.ForcedEnergySupContract : Prop

Sup-in-time L² bound for θ − θ_M, with the hypotheses of the stream-difference estimate.

Equations

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

def AVenhance.Infra.FullTheorem.HeatApproxH1Contract : Prop

analytic_approximation with the additional H¹ contraction conjunct.

Equations

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

def AVenhance.Infra.FullTheorem.WeakDifferenceContract : Prop

Two weak solutions with the same bounded divergence-free drift: the L² distance does not exceed the L² distance of the data, at every time in [0,1].

Equations

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