Lowering the Hölder exponent of a drift

If b lies in IsHolderClass a and 0 < α < a, then b lies in IsHolderClass α, and t ↦ b(t,·) is continuous into the spatial C^{0,α} seminorm. The second statement is the interpolation min(A, B) ≤ A^{1-θ} B^θ with θ = α / a, applied to the two bounds |g(x) - g(y)| ≤ 2C|t - s|^a and |g(x) - g(y)| ≤ 2C'|x - y|^a for g = b(t,·) - b(s,·).

theorem AVenhance.Infra.Drift.le_rpow_mul_rpow_of_le_of_le {z P Q θ : ℝ} (hP : 0 ≤ P) (hQ : 0 ≤ Q) (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) (hzP : z ≤ P) (hzQ : z ≤ Q) : z ≤ P ^ (1 - θ) * Q ^ θ

min(P, Q) ≤ P^{1-θ} Q^θ for P, Q ≥ 0 and θ ∈ [0,1].

theorem AVenhance.Infra.Drift.rpow_interp_eq {p q u v a θ : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hu : 0 ≤ u) (hv : 0 ≤ v) : (p * u ^ a) ^ (1 - θ) * (q * v ^ a) ^ θ = p ^ (1 - θ) * q ^ θ * (u ^ (a * (1 - θ)) * v ^ (a * θ))

(p u^a)^{1-θ} (q v^a)^θ = p^{1-θ} q^θ u^{a(1-θ)} v^{aθ} for nonnegative p, q, u, v.

theorem AVenhance.Infra.Drift.rpow_le_rpow_of_le_one {x α a : ℝ} (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) (hα : 0 ≤ α) (hαa : α ≤ a) : x ^ a ≤ x ^ α

On [0,1], a larger exponent gives a smaller power.

theorem AVenhance.Infra.Drift.abs_sub_le_one_of_mem_Icc {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) : |s - t| ≤ 1

theorem AVenhance.Infra.Drift.isHolderClass_mono {a α : ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : IsHolderClass a b) (hα : 0 < α) (hαa : α ≤ a) : IsHolderClass α b

Lowering the exponent of the drift class.

theorem AVenhance.Infra.Drift.isContinuousIntoHolder_of_lt {a α : ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : IsHolderClass a b) (hα : 0 < α) (hαa : α < a) : IsContinuousIntoHolder α b

A drift of class IsHolderClass a is continuous in time into the spatial C^{0,α} seminorm for every 0 < α < a.