Smoothness of partial derivatives (shared helpers of the no-selection inputs)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.smoothPartial {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (v : Homogenization.Vec 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (fderiv ℝ ψ x) v

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.contDiff_spaceGrad_coord {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceGrad ψ x i

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.contDiff_spaceGrad {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : ContDiff ℝ (↑⊤) (spaceGrad ψ)