Documentation

Complexity.Foundations.BooleanAnalysis.HarmonicMean

Korten's harmonic mean transform #

The harmonic mean transform of a function on the cube (harmonicTransform, Korten, Definition 5) projects the function to a set of selected coordinates and takes the harmonic mean (Cslib.harmonicMean) of the projection. It is the harmonic mean of the marginal on the selected coordinates (harmonicTransform_eq_harmonicMean_coordinateMarginal), and it is concave in the function, antitone in the selected set and at most the mean Korten, Corollary 1. Korten's inequality bounds the expected square root of a function by the expected square root of its transform at a random set containing each coordinate with probability 1 / 4 Korten, Lemma 12 (expect_sqrt_le_bernoulliAverage_sqrt_harmonicTransform), which gives the sampling estimate in the proof of Lemma 10 (harmonicTransform_good_probability). The sparse sampling conclusion of Lemma 10 is BitString.harmonicTransform_sparse_good_probability.

Main definitions #

Main results #

References #

The harmonic mean transform #

A coordinate set is its Boolean membership function. The transform is represented on the full cube: projectionAverage f selected depends only on the selected coordinates, and averaging on the full cube gives each projected pattern the same multiplicity, so its harmonic mean is the harmonic mean over the projected patterns (harmonicTransform_eq_harmonicMean_coordinateMarginal).

source
noncomputable def Cslib.BitString.harmonicTransform {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected : ι → Bool) :
ℝ

Korten's harmonic mean transform Korten, Definition 5: the harmonic mean of the projection of f to the selected coordinates, represented on the full cube.

Instances For
    source
    theorem Cslib.BitString.harmonicTransform_reindex {ι : 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)

    An equivalence of coordinate types commutes with the harmonic transform.

    source
    theorem Cslib.BitString.harmonicTransform_eq_harmonicMean_coordinateMarginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected : ι → Bool) :
    harmonicTransform f selected = harmonicMean (coordinateMarginal f selected)

    The transform agrees with Definition 5 on the actual projected cube; repeating each pattern on the full cube does not change its harmonic mean.

    source
    theorem Cslib.BitString.harmonicTransform_variational {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected : ι → Bool) :
    harmonicTransform f selected = sInf {a : ℝ | ∃ (w : ({ i : ι // selected i = true } → Bool) → ℝ), (∀ (z : { i : ι // selected i = true } → Bool), 0 ≤ w z) ∧ (Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => w z) = 1 ∧ (Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => coordinateMarginal f selected z * w z ^ 2) = a}

    Lemma 11 on the selected-coordinate cube, with nonnegative weights of mean one.

    source
    theorem Cslib.BitString.harmonicTransform_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected : ι → Bool) :
    0 ≤ harmonicTransform f selected

    The harmonic transform is nonnegative on nonnegative functions.

    source
    theorem Cslib.BitString.harmonicTransform_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : ℝ) (selected : ι → Bool) :
    harmonicTransform (fun (x : ι → Bool) => c) selected = c

    Constants are fixed by the harmonic transform.

    source
    theorem Cslib.BitString.harmonicTransform_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) :
    (harmonicTransform f fun (x : ι) => false) = Finset.univ.expect fun (x : ι → Bool) => f x

    Selecting no coordinates gives the ordinary mean.

    source
    theorem Cslib.BitString.harmonicTransform_full {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) :
    (harmonicTransform f fun (x : ι) => true) = harmonicMean f

    Selecting all coordinates gives the harmonic mean of the original function.

    source
    theorem Cslib.BitString.concaveOn_harmonicTransform {ι : Type u_1} [Fintype ι] [DecidableEq ι] (selected : ι → Bool) :
    ConcaveOn ℝ (Set.Ici 0) fun (f : (ι → Bool) → ℝ) => harmonicTransform f selected

    The transform is concave in the function Korten, Corollary 1: for every selected set, it is concave on nonnegative functions.

    Splitting off the first coordinate #

    The proofs of the antitonicity of the transform and of Korten's Lemma 12 are inductions on the dimension, on the cube Fin n → Bool, which split off the first coordinate.

    The transform is antitone in the selected set #

    source
    theorem Cslib.BitString.harmonicTransform_antitone {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) :
    Antitone (harmonicTransform f)

    Selecting more coordinates decreases the harmonic transform Korten, Corollary 1.

    source
    theorem Cslib.BitString.harmonicTransform_le_expect {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected : ι → Bool) :
    harmonicTransform f selected ≤ Finset.univ.expect fun (x : ι → Bool) => f x

    The harmonic transform is at most the ordinary mean Korten, Corollary 1.

    Korten's harmonic mean inequality #

    The inequality Korten, Lemma 12 follows from a scalar inequality by induction on the dimension, using concavity of the harmonic mean. No strict-positivity assumption is needed.

    source
    theorem Cslib.BitString.expect_sqrt_le_bernoulliAverage_sqrt_harmonicTransform {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) :
    (Finset.univ.expect fun (x : ι → Bool) => √(f x)) ≤ bernoulliAverage (1 / 4) fun (selected : ι → Bool) => √(harmonicTransform f selected)

    Korten's harmonic mean inequality Korten, Lemma 12: on the 1/4-biased coordinate cube, the mean square root of the harmonic transform dominates the uniform mean square root of f.

    Dense distributions and good coordinate projections #

    The first probability estimate in the proof of Korten's Lemma 10, before transference to a sparse coordinate set. We use a pointwise density bound B instead of writing it as 2 ^ k.

    source
    theorem Cslib.BitString.harmonicTransform_good_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (hmean : (Finset.univ.expect fun (x : ι → Bool) => f x) = 1) {B : ℝ} (hB : 1 ≤ B) (hbound : ∀ (x : ι → Bool), f x ≤ B) :
    1 / (2 * √B) ≤ bernoulliAverage (1 / 4) fun (selected : ι → Bool) => if 1 / (4 * B) ≤ harmonicTransform f selected then 1 else 0

    Intermediate estimate in the proof of Lemma 10: a normalized density bounded by B has harmonic transform at least 1 / (4 * B) with probability at least 1 / (2 * sqrt B) under 1/4-coordinate sampling. The LightPatterns module transfers this estimate to sparse sampling.

    source
    theorem Cslib.BitString.coordinateMarginal_light_fraction_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected : ι → Bool) {a b : ℝ} (ha : 0 < a) (ha' : a ≤ harmonicTransform f selected) (hb : 0 ≤ b) :
    (Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => if coordinateMarginal f selected z ≤ b then 1 else 0) ≤ b / a

    A positive transform lower bound bounds the fraction of light projected patterns. The expectation ranges over the actual selected-coordinate cube.