TCSLib

222 Boolean Analysis — Interpolation

222.1 Overview

Symmetric averages of profile-vector lengths admit a contraction inequality whenever the profile satisfies the scalar two-point bound. The auxiliary squared-length parameter records the remaining displacement variance.

222.2 Declarations

Definition 222.1 Symmetric average length
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). The symmetric average length is \(L(t,c)\).

Definition 222.2 Symmetric interpolation deficit
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). The interpolation deficit is \(\Delta (t,c)=L(t,c)-L(1,c+b^2(1-t^2))\).

Lemma 222.3 Bounded doubling principle
✓
#

Lean declarations

Let \(s\) be a subset of a set \(X\) and \(f:X\to \mathbb R\). If \(f(s)\) is bounded above and every \(x\in s\) admits \(y\in s\) with \(f(x)\le f(y)/2\), then \(f(x)\le 0\) for all \(x\in s\).

Lemma 222.4 Subadditivity of the square root
✓
#

Lean declarations

For any real \(x,y\ge 0\), \(\sqrt{x+y}\le \sqrt x+\sqrt y\).

Lemma 222.5 Even symmetric displacement
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). For all parameters, \(L(-t,c)=L(t,c)\).

Lemma 222.6 Absolute symmetric displacement
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). For all parameters, \(L(|t|,c)=L(t,c)\).

Lemma 222.7 Probability along a symmetric segment
✓
#

Lean declarations

If \(a+b,a-b\in [0,1]\) and \(-1\le t\le 1\), then \(a+tb\in [0,1]\).

Lemma 222.8 Concavity in additional squared length
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). For every \(P,a,b,u,v\), the function \(c\mapsto L(1,c)\) is concave on \([0,\infty )\).

Lemma 222.9 Continuity in the displacement
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). If \(P\) is continuous on \([0,1]\) and \(a+b,a-b\in [0,1]\), then \(t\mapsto L(t,0)\) is continuous on \([0,1]\).

Lemma 222.10 Cost of an additional squared length
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). For any real \(t\) and \(c\ge 0\), \(L(t,c)\le \sqrt c+L(t,0)\).

Lemma 222.11 Adaptive midpoint length bound
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). Assume \(P\ge 0\) on \([0,1]\) and, whenever \(z\pm d\in [0,1]\), \(P(z)\le \bigl(\sqrt{P(z+d)^2+d^2}+\sqrt{P(z-d)^2+d^2}\bigr)/2\). If \(a\pm b\in [0,1]\), \(0\le t\le 1\), and \(c\ge 0\), then \(L(t,c)\le \bigl(L(1,c+((1-t)b)^2)+L(2t-1,c+((1-t)b)^2)\bigr)/2\).

Lemma 222.12 Lower bound by additional length
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). For every real \(t,c\), \(\sqrt c\le L(t,c)\), with the real square root taken to be zero on negative arguments.

Lemma 222.13 Bounded interpolation deficits
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). If \(P\) is continuous on \([0,1]\) and \(a\pm b\in [0,1]\), the set \(\{ L(t,c)-L(1,c+b^2(1-t^2)):0\le t\le 1,\ c\ge 0\} \) is bounded above.

Lemma 222.14 Deficit after one adaptive step
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). Assume \(P\ge 0\) on \([0,1]\) and, whenever \(z\pm d\in [0,1]\), \(P(z)\le \bigl(\sqrt{P(z+d)^2+d^2}+\sqrt{P(z-d)^2+d^2}\bigr)/2\). Put \(\Delta (t,c)=L(t,c)-L(1,c+b^2(1-t^2))\). If \(a\pm b\in [0,1]\), \(0\le t\le 1\), and \(c\ge 0\), then \(\Delta (t,c)\le \Delta (|2t-1|,c+((1-t)b)^2)/2\).

Lemma 222.15 Symmetric endpoint length comparison
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). Assume \(P\ge 0\) on \([0,1]\) and, whenever \(z\pm d\in [0,1]\), \(P(z)\le \bigl(\sqrt{P(z+d)^2+d^2}+\sqrt{P(z-d)^2+d^2}\bigr)/2\). If \(P\) is also continuous on \([0,1]\), \(a\pm b\in [0,1]\), \(0\le t\le 1\), and \(c\ge 0\), then \(L(t,c)\le L(1,c+b^2(1-t^2))\).

Lemma 222.16 Symmetric pair contraction
✓
#

Lean declarations

For a profile \(P:\mathbb R\to \mathbb R\), \(a,b,t,c\in \mathbb R\), and \(u,v\in \mathbb R^m\), define \(L(t,c)=\frac12\bigl(\sqrt{P(a+tb)^2+c+\| u+tv\| _2^2}+\sqrt{P(a-tb)^2+c+\| u-tv\| _2^2}\bigr)\). Assume \(P\ge 0\) on \([0,1]\) and, whenever \(z\pm d\in [0,1]\), \(P(z)\le \bigl(\sqrt{P(z+d)^2+d^2}+\sqrt{P(z-d)^2+d^2}\bigr)/2\). If \(P\) is also continuous on \([0,1]\), \(a\pm b\in [0,1]\), and \(0\le t\le 1\), then \(L(t,(tb)^2)\le L(1,b^2)\).