CosineDatumContract

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cosDatum_periodic (n : ℕ) (c : ℝ) : IsZ2Periodic fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cosDatum_meanZero (n : ℕ) (hn : 1 ≤ n) (c : ℝ) : Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cosDatum_l2 (n : ℕ) (hn : 1 ≤ n) (c : ℝ) : (l2NormSq fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0)) = c ^ 2 / 2

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cosDatum_spaceGrad (n : ℕ) (c : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0)) x i = (if i = 0 then 1 else 0) * (c * (2 * Real.pi * ↑n) * Real.cos (2 * Real.pi * ↑n * x 0 + Real.pi / 2))

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cosDatum_gradNormSq (n : ℕ) (hn : 1 ≤ n) (c : ℝ) : gradNormSq (spaceGrad fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0)) = 4 * Real.pi ^ 2 * ↑n ^ 2 * (c ^ 2 / 2)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cosDatum_hessNormSq (n : ℕ) (hn : 1 ≤ n) (c : ℝ) : (hessNormSq fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0)) = (2 * Real.pi * ↑n) ^ 4 * (c ^ 2 / 2)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cosDatum_analytic (n : ℕ) (hn : 1 ≤ n) (c : ℝ) : IsThetaAnalytic (1 / (2 * Real.pi * ↑n)) fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.cosineDatum : CosineDatumContract