Triangle inequalities for the actual space-time gradient norm.

theorem AVenhance.Infra.Section5.RelativeError.RelativeNorms.relative_timeCube_integrable {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContinuousOn f (Set.Ici 0 ×ˢ Set.univ)) : MeasureTheory.IntegrableOn f timeCube MeasureTheory.volume

theorem AVenhance.Infra.Section5.RelativeError.relative_vecDot_continuousOn {f g : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} {s : Set (ℝ × Homogenization.Vec 2)} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (f p) (g p)) s

theorem AVenhance.Infra.Section5.RelativeError.relative_gradient_norm_add_le {f g : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => f p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hg : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => g p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => f t x + g t x) ≤ √(spaceTimeGradNormSq f) + √(spaceTimeGradNormSq g)

theorem AVenhance.Infra.Section5.RelativeError.relative_gradient_norm_neg (f : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : (spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => -f t x) = spaceTimeGradNormSq f

theorem AVenhance.Infra.Section5.RelativeError.relative_gradient_norm_sub_le {f g : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => f p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hg : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => g p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : |√(spaceTimeGradNormSq f) - √(spaceTimeGradNormSq g)| ≤ √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => f t x - g t x)

theorem AVenhance.Infra.Section5.RelativeError.relative_gradient_memLp_of_continuous {f : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => f p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => f p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)

Joint closed-half-line continuity supplies coordinate L2 integrability.

theorem AVenhance.Infra.Section5.RelativeError.relative_gradient_dot_integrable {f g : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => f p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) (hg : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => g p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (f p.1 p.2) (g p.1 p.2)) timeCube MeasureTheory.volume

Dot products of genuine coordinate L2 fields are integrable.

theorem AVenhance.Infra.Section5.RelativeError.relative_gradient_norm_sub_le_of_memLp {f g : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => f p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) (hg : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => g p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) : |√(spaceTimeGradNormSq f) - √(spaceTimeGradNormSq g)| ≤ √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => f t x - g t x)

Reverse gradient triangle inequality using integrability, with no time-zero regularity premise.