Marginal semantics of the harmonic mean transform #
Splitting the cube into selected and unselected coordinates identifies the full-cube representation with the paper's averages on projected patterns.
theorem
Complexity.BooleanAnalysis.projectionAverage_eq_coordinateMarginal_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(f : (ι → Bool) → ℝ)
(selected x : ι → Bool)
:
projectionAverage f selected x = coordinateMarginal f selected fun (i : { i : ι // selected i = true }) => x ↑i
theorem
Complexity.BooleanAnalysis.expect_coordinateMarginal_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(f : (ι → Bool) → ℝ)
(selected : ι → Bool)
:
(Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => coordinateMarginal f selected z) = Finset.univ.expect fun (x : ι → Bool) => f x
theorem
Complexity.BooleanAnalysis.harmonicTransform_eq_harmonicMean_coordinateMarginal_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(f : (ι → Bool) → ℝ)
(selected : ι → Bool)
: