L² bookkeeping for Lemma r.LeBron #
Triangle inequalities for continuous slices and slice continuity of classical solutions.
theorem
AVenhance.Infra.FullTheorem.sqrt_l2NormSq_sub_le
{f g : Homogenization.Vec 2 → ℝ}
(hf : Continuous f)
(hg : Continuous g)
:
Triangle inequality for a difference of continuous functions.
theorem
AVenhance.Infra.FullTheorem.IsClassicalSol.continuous_slice
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F : ℝ → Homogenization.Vec 2 → ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(h : IsClassicalSol b κ F θ₀ θ)
{t : ℝ}
(ht : 0 ≤ t)
:
Continuous (θ t)
Time slices of a classical solution are continuous (at times t ≥ 0).
theorem
AVenhance.Infra.FullTheorem.difference_bounds
{θm θprev : ℝ → Homogenization.Vec 2 → ℝ}
(hcm : ∀ t ∈ Set.Icc 0 1, Continuous (θm t))
(hcp : ∀ t ∈ Set.Icc 0 1, Continuous (θprev t))
{A Sm Sp : ℝ}
(hsup : ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - θprev t x) ≤ A)
(hm :
∀ s ∈ Set.Icc 0 1,
∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - θm s x) ≤ Sm * |t - s| ^ (1 / 4))
(hp :
∀ s ∈ Set.Icc 0 1,
∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θprev t x - θprev s x) ≤ Sp * |t - s| ^ (1 / 4))
{s t : ℝ}
(hs : s ∈ Set.Icc 0 1)
(ht : t ∈ Set.Icc 0 1)
:
The sup and the 1/4-Hölder bounds of the difference θm - θprev from the pieces.