Statement file: IsHolderClass (Roots). This file contains exactly one declaration of the formalization's public statement surface.

def AVenhance.IsHolderClass (α : ℝ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

b is a bounded, continuous, ℤ²-periodic drift on [0,1] × 𝕋² that is Hölder continuous of exponent α in space and in time.

Equations

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