Literal restatements of the main theorem, classical well-posedness and stream-function

estimates statements

Each …Statement is the proposition of the corresponding public statement, restated (theorem binders turned into ∀ binders; hypothesis binder names that the body does not mention carry a _ prefix to satisfy the unused-variable linter — alpha-equivalent, so exact applies), so that anomalous_dissipation_of_keystones can be closed by exact once the three estimates are proved. The statement files themselves are never imported.

def AVenhance.Infra.Section5.Integration.AnomalousDissipationStatement : Prop

The main theorem with the drift class IsHolderClass only, its binders as ∀. The public statement AVenhance.anomalous_dissipation adds IsContinuousIntoHolder, obtained from this one at a larger exponent by Infra.Drift.isContinuousIntoHolder_of_lt.

Equations

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

def AVenhance.Infra.Section5.Integration.ClassicalWellposedStatement : Prop

Verbatim proposition of the public statement AVenhance.classical_wellposed (classical well-posedness), its binders as ∀.

Equations

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

def AVenhance.Infra.Section5.Integration.LimitFieldRegularStatement (β : ℝ) : Prop

Verbatim proposition of the public statement AVenhance.limit_field_regular (stream-function estimates).

Equations

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