L²(𝕋²) bookkeeping for the ansatz estimate e.tildethetam.to.Tm

Elementary facts about the l2NormSq for continuous functions: the square of a continuous function is integrable on the unit cube, pointwise domination by a continuous function dominates l2NormSq, scaling by a nonnegative constant, and the triangle inequality for |f| + |g|.

theorem AVenhance.Infra.Section5.Integration.integrableOn_sq_unitCube_of_continuous {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => f x ^ 2) unitCube MeasureTheory.volume

The square of a continuous function is integrable on the unit cube.

theorem AVenhance.Infra.Section5.Integration.sqrt_l2NormSq_le_of_abs_le {f g : Homogenization.Vec 2 → ℝ} (hg : Continuous g) (h : ∀ (x : Homogenization.Vec 2), |f x| ≤ g x) : √(l2NormSq f) ≤ √(l2NormSq g)

Pointwise domination by a continuous function dominates the L² norm.

theorem AVenhance.Infra.Section5.Integration.sqrt_l2NormSq_const_mul {c : ℝ} (hc : 0 ≤ c) (f : Homogenization.Vec 2 → ℝ) : √(l2NormSq fun (x : Homogenization.Vec 2) => c * f x) = c * √(l2NormSq f)

theorem AVenhance.Infra.Section5.Integration.l2NormSq_abs (f : Homogenization.Vec 2 → ℝ) : (l2NormSq fun (x : Homogenization.Vec 2) => |f x|) = l2NormSq f

theorem AVenhance.Infra.Section5.Integration.sqrt_l2NormSq_abs_add_le {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) : √(l2NormSq fun (x : Homogenization.Vec 2) => |f x| + |g x|) ≤ √(l2NormSq f) + √(l2NormSq g)

Triangle inequality for |f| + |g| with continuous f, g.

theorem AVenhance.Infra.Section5.Integration.sqrt_l2NormSq_add_le_of_continuous {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) : √(l2NormSq fun (x : Homogenization.Vec 2) => f x + g x) ≤ √(l2NormSq f) + √(l2NormSq g)

Triangle inequality for continuous f, g.