Integrals of functions of x₀ over the unit cube, and ∫ cos² of the cosine data

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.integral_unitCube_coord0 (G : ℝ → ℝ) : ∫ (x : Homogenization.Vec 2) in unitCube, G (x 0) = ∫ (s : ℝ) in Set.Ioo 0 1, G s

A function of the first coordinate integrates over the unit cube as a one-dimensional integral over (0,1).

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.integral_cos_sq_phase (n : ℕ) (hn : 1 ≤ n) (φ : ℝ) : ∫ (s : ℝ) in Set.Ioo 0 1, Real.cos (2 * Real.pi * ↑n * s + φ) ^ 2 = 1 / 2

∫_0^1 cos²(2π n s + φ) ds = 1/2.

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.integral_unitCube_cos_sq (n : ℕ) (hn : 1 ≤ n) (A φ : ℝ) : ∫ (x : Homogenization.Vec 2) in unitCube, (A * Real.cos (2 * Real.pi * ↑n * x 0 + φ)) ^ 2 = A ^ 2 / 2

∫_{cube} (A cos(2π n x₀ + φ))² = A²/2.