Coordinate splitting for the harmonic mean transform

Finite product calculations used in the induction in Korten's Lemma 12.

theorem Complexity.BooleanAnalysis.expect_cons_internal {n : ℕ} (f : (Fin (n + 1) → Bool) → ℝ) : (Finset.univ.expect fun (x : Fin (n + 1) → Bool) => f x) = ((Finset.univ.expect fun (x : Fin n → Bool) => f (Fin.cons false x)) + Finset.univ.expect fun (x : Fin n → Bool) => f (Fin.cons true x)) / 2

theorem Complexity.BooleanAnalysis.projectionAverage_nonneg_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected x : ι → Bool) : 0 ≤ projectionAverage f selected x

theorem Complexity.BooleanAnalysis.harmonicTransform_nonneg_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected : ι → Bool) : 0 ≤ harmonicTransform f selected

theorem Complexity.BooleanAnalysis.harmonicTransform_const_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : ℝ) (selected : ι → Bool) : harmonicTransform (fun (x : ι → Bool) => c) selected = c

theorem Complexity.BooleanAnalysis.projectionAverage_midpoint_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → ℝ) (selected x : ι → Bool) : projectionAverage (fun (x : ι → Bool) => (f x + g x) / 2) selected x = (projectionAverage f selected x + projectionAverage g selected x) / 2

theorem Complexity.BooleanAnalysis.projectionAverage_cons_false_internal {n : ℕ} (f : (Fin (n + 1) → Bool) → ℝ) (selected x : Fin n → Bool) (b : Bool) : projectionAverage f (Fin.cons false selected) (Fin.cons b x) = projectionAverage (fun (x : Fin n → Bool) => (f (Fin.cons false x) + f (Fin.cons true x)) / 2) selected x

theorem Complexity.BooleanAnalysis.projectionAverage_cons_true_internal {n : ℕ} (f : (Fin (n + 1) → Bool) → ℝ) (selected x : Fin n → Bool) (b : Bool) : projectionAverage f (Fin.cons true selected) (Fin.cons b x) = projectionAverage (fun (x : Fin n → Bool) => f (Fin.cons b x)) selected x

theorem Complexity.BooleanAnalysis.harmonicTransform_cons_false_internal {n : ℕ} (f : (Fin (n + 1) → Bool) → ℝ) (selected : Fin n → Bool) : harmonicTransform f (Fin.cons false selected) = harmonicTransform (fun (x : Fin n → Bool) => (f (Fin.cons false x) + f (Fin.cons true x)) / 2) selected

theorem Complexity.BooleanAnalysis.harmonicTransform_cons_true_internal {n : ℕ} {f : (Fin (n + 1) → Bool) → ℝ} (hf : ∀ (x : Fin (n + 1) → Bool), 0 ≤ f x) (selected : Fin n → Bool) : harmonicTransform f (Fin.cons true selected) = 2 * harmonicTransform (fun (x : Fin n → Bool) => f (Fin.cons false x)) selected * harmonicTransform (fun (x : Fin n → Bool) => f (Fin.cons true x)) selected / (harmonicTransform (fun (x : Fin n → Bool) => f (Fin.cons false x)) selected + harmonicTransform (fun (x : Fin n → Bool) => f (Fin.cons true x)) selected)

theorem Complexity.BooleanAnalysis.harmonicTransform_midpoint_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f g : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (hg : ∀ (x : ι → Bool), 0 ≤ g x) (selected : ι → Bool) : (harmonicTransform f selected + harmonicTransform g selected) / 2 ≤ harmonicTransform (fun (x : ι → Bool) => (f x + g x) / 2) selected