Public statement.

def AVenhance.IsHolderTimeL2 (μ H : ℝ) (θ : ℝ → Homogenization.Vec 2 → ℝ) : Prop

Time-Hölder seminorm bound on [0,1] with values in L²(𝕋²) (unit cell): ‖θ(t) − θ(s)‖_{L²} ≤ H |t − s|^μ for all s, t ∈ [0,1].

Equations

• AVenhance.IsHolderTimeL2 μ H θ = ∀ s ∈ Set.Icc 0 1, ∀ t ∈ Set.Icc 0 1, √(AVenhance.l2NormSq fun (x : Homogenization.Vec 2) => θ t x - θ s x) ≤ H * |t - s| ^ μ