Reindexing coordinate projections

Transport the harmonic transform along an equivalence of finite coordinate types. This lets results proved by induction on Fin n apply inside fibers.

theorem Complexity.BooleanAnalysis.projectionAverage_reindex_internal {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (f : (κ → Bool) → ℝ) (s x : ι → Bool) : projectionAverage (fun (y : ι → Bool) => f fun (j : κ) => y (e.symm j)) s x = projectionAverage f (fun (j : κ) => s (e.symm j)) fun (j : κ) => x (e.symm j)

theorem Complexity.BooleanAnalysis.harmonicTransform_reindex_internal {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (f : (κ → Bool) → ℝ) (s : ι → Bool) : harmonicTransform (fun (y : ι → Bool) => f fun (j : κ) => y (e.symm j)) s = harmonicTransform f fun (j : κ) => s (e.symm j)