Level functions and their rows

For a real function f on the cube and a real number t, lev f t is the level function g_t = 1_{f > t}. If a x is a row of f at x, then levRow f a t x, which is a x / |f x - t| (and the all-ones vector when f x = t), is a row of g_t at x (isRow_levRow; the cases f x ≠ t and f x = t are parts (iii) and (i) of Lemma 2.4 of the paper). These are the rows λ^{t,x} of Section 7.1 of the paper.

noncomputable def AaronsonAmbainis.Level.lev {ι : Type u_1} (f : Cube ι → ℝ) (t : ℝ) : Cube ι → Bool

The level function g_t = 1_{f > t}.

Equations

• AaronsonAmbainis.Level.lev f t x = decide (t < f x)

noncomputable def AaronsonAmbainis.Level.levRow {ι : Type u_1} (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) (t : ℝ) : Cube ι → ι → ℝ

The row of g_t at x built from the row a x of f: a x / |f x - t| (and the all-ones vector when f x = t).

Equations

• AaronsonAmbainis.Level.levRow f a t x j = if f x = t then 1 else a x j / |f x - t|

theorem AaronsonAmbainis.Level.abs_sub_le_of_lev_ne {ι : Type u_1} {f : Cube ι → ℝ} {t : ℝ} {x y : Cube ι} (h : lev f t y ≠ lev f t x) : |f x - t| ≤ |f x - f y|

If g_t separates x and y then t lies weakly between f x and f y.

theorem AaronsonAmbainis.Level.isRow_levRow {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} {a : Cube ι → ι → ℝ} (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) (t : ℝ) (x : Cube ι) : IsRow (lev f t) x (levRow f a t x)

levRow f a t x is a row of g_t at x.