Statement of the combined main theorem (anomalous_dissipation_full)

AnomalousDissipationFullStatement is the proposition of AVenhance.anomalous_dissipation_full with the drift class IsHolderClass only (without IsContinuousIntoHolder, which the public statement obtains at a larger exponent), with the binders (α) (hα₀) (hα₁) turned into a leading ∀.

def AVenhance.Infra.FullTheorem.AnomalousDissipationFullStatement : Prop

The combined main theorem with the drift class IsHolderClass only.

Equations

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