Hölder upgrade by interpolation

A function with small sup-L² norm and bounded μ-Hölder seminorm has small C^{0,μ/2}([0,1];L²) norm; and the limit of uniformly μ-Hölder functions is μ-Hölder.

theorem AVenhance.Infra.FullTheorem.holderL2Le_of_small {μ H α : ℝ} {f : ℝ → Homogenization.Vec 2 → ℝ} (hmem : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (f t)) (hsup : ∀ t ∈ Set.Icc 0 1, √(l2NormSq (f t)) ≤ α) (hhol : IsHolderTimeL2 μ H f) : HolderTimeL2Le (μ / 2) (α + √(2 * α * H)) f

theorem AVenhance.Infra.FullTheorem.exists_small_alpha {H : ℝ} (hH : 0 ≤ H) {η : ℝ} (hη : 0 < η) : ∃ (α : ℝ), 0 < α ∧ α + √(2 * α * H) ≤ η

theorem AVenhance.Infra.FullTheorem.holder_of_limit {μ H : ℝ} {f : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {Θ : ℝ → Homogenization.Vec 2 → ℝ} (hmf : ∀ (j : ℕ), ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (f j t)) (hmΘ : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (Θ t)) (hlim : ∀ (η : ℝ), 0 < η → ∃ (N : ℕ), ∀ j ≥ N, ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => f j t x - Θ t x) ≤ η) (hH : ∀ (j : ℕ), IsHolderTimeL2 μ H (f j)) : IsHolderTimeL2 μ H Θ

Passing a uniform L² limit through the time-Hölder seminorm.

theorem AVenhance.Infra.FullTheorem.abs_sqrt_l2_sub_le {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : |√(l2NormSq f) - √(l2NormSq g)| ≤ √(l2NormSq fun (x : Homogenization.Vec 2) => f x - g x)

Reverse triangle inequality for L² norms of L² functions.