H¹ case of r.LeBron.2: the approximation argument

Given the analytic-case Hölder bound (hana), the L² contraction of differences (hdiff), existence (hexist) and the energy bound (henergy) for a fixed drift b and κ, a weak solution with mean-zero H¹ data is ν-Hölder in time with ν = μ/(1+p) and constant ∝ ‖θ₀‖_{H¹}.

theorem AVenhance.Infra.FullTheorem.UniformH1.holder_of_analytic {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ μ p K : ℝ} (hμ : 0 < μ) (hp : 0 ≤ p) (hK : 0 ≤ K) (happrox : HeatApproxH1Contract) (hana : ∀ (R : ℝ), 0 < R → ∀ (g : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) g → IsZ2Periodic g → Homogenization.MeanZeroOn unitCube g → IsThetaAnalytic R g → ∀ (θ' : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ g θ' → IsHolderTimeL2 μ (K * (1 + R ^ (-p)) * √(l2NormSq g + gradNormSq (spaceGrad g))) θ') (hdiff : ∀ (f g : Homogenization.Vec 2 → ℝ), Homogenization.MemL2On unitCube f → Homogenization.MemL2On unitCube g → ∀ (θ θ' : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ f θ → IsWeakSolution b κ g θ' → ∀ t ∈ Set.Icc 0 1, (l2NormSq fun (x : Homogenization.Vec 2) => θ t x - θ' t x) ≤ l2NormSq fun (x : Homogenization.Vec 2) => f x - g x) (hexist : ∀ (g : Homogenization.Vec 2 → ℝ), Homogenization.MemL2On unitCube g → ∃ (θ' : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ g θ') (henergy : ∀ (f : Homogenization.Vec 2 → ℝ), Homogenization.MemL2On unitCube f → ∀ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ f θ → ∀ t ∈ Set.Icc 0 1, l2NormSq (θ t) ≤ l2NormSq f) {θ₀ : Homogenization.Vec 2 → ℝ} {Dθ₀ : Homogenization.Vec 2 → Homogenization.Vec 2} (hθ₀ : IsPeriodicH1With θ₀ Dθ₀) (hm : Homogenization.MeanZeroOn unitCube θ₀) {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsWeakSolution b κ θ₀ θ) : HolderTimeL2Le (μ / (1 + p)) ((11 + 4 * 2 ^ p * K) * √(l2NormSq θ₀ + gradNormSq Dθ₀)) θ