Statement file: IsContinuousIntoHolder (Roots).
This file contains exactly one declaration of the formalization's public statement surface.
def
AVenhance.IsContinuousIntoHolder
(α : ℝ)
(b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
:
t ↦ b(t,·) is continuous on [0,1] for the spatial α-Hölder seminorm: for every
s ∈ [0,1] and ε > 0 there is δ > 0 such that [b(t,·) - b(s,·)]_{C^{0,α}} ≤ ε whenever
t ∈ [0,1] and |t - s| < δ. Together with IsHolderClass α b (which gives continuity in
time for the supremum norm) this is the class C⁰_t C^{0,α}_x ∩ C^{0,α}_t C⁰_x of the paper.
Equations
- One or more equations did not get rendered due to their size.