Helpers for the H¹ case of r.LeBron.2

Abstract-real rpow algebra, L² triangle inequality for differences, and positivity of the gradient for mean-zero H¹ data.

theorem AVenhance.Infra.FullTheorem.UniformH1.rpow_scale_identity {h ν μ p : ℝ} (hh : 0 < h) (hμ : μ = ν * (1 + p)) : (h ^ ν / 2) ^ (-p) * h ^ μ = 2 ^ p * h ^ ν

(h^ν / 2)^{-p} · h^μ = 2^p · h^ν when μ = ν (1 + p).

theorem AVenhance.Infra.FullTheorem.UniformH1.one_le_scale {h ν p : ℝ} (hh : 0 < h) (hh1 : h ≤ 1) (hν : 0 ≤ ν) (hp : 0 ≤ p) : 1 ≤ (h ^ ν / 2) ^ (-p)

1 ≤ (h^ν / 2)^{-p} for 0 < h ≤ 1, p ≥ 0, 0 < ν.

theorem AVenhance.Infra.FullTheorem.UniformH1.sqrt_l2_sub_le {a b : Homogenization.Vec 2 → ℝ} (ha : Homogenization.MemL2On unitCube a) (hb : Homogenization.MemL2On unitCube b) : √(l2NormSq fun (x : Homogenization.Vec 2) => a x - b x) ≤ √(l2NormSq a) + √(l2NormSq b)

Triangle inequality for a difference.

theorem AVenhance.Infra.FullTheorem.UniformH1.sqrt_l2_tri {a b c : Homogenization.Vec 2 → ℝ} (ha : Homogenization.MemL2On unitCube a) (hb : Homogenization.MemL2On unitCube b) (hc : Homogenization.MemL2On unitCube c) : √(l2NormSq fun (x : Homogenization.Vec 2) => a x - c x) ≤ √(l2NormSq fun (x : Homogenization.Vec 2) => a x - b x) + √(l2NormSq fun (x : Homogenization.Vec 2) => b x - c x)

theorem AVenhance.Infra.FullTheorem.UniformH1.l2NormSq_nonneg (f : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq f

theorem AVenhance.Infra.FullTheorem.UniformH1.gradNormSq_nonneg (Df : Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ gradNormSq Df

theorem AVenhance.Infra.FullTheorem.UniformH1.gradient_pos {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) (hm : Homogenization.MeanZeroOn unitCube f) (hA : 0 < l2NormSq f) : 0 < gradNormSq Df