ScalarFunction

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the scalar function f(x) = x⁻¹ (x-1)²

This file isolates, over abstract reals, the scalar analysis used in the proof of the second inequality of e.bound.Lambdas.by.Es in ABK26.

The printed proof introduces f(x) := x^{-1}(x-1)^2, observes that f is the eigenvalue function of the operator inequalities e.xminusonetimesxminusonesquared.sstar and e.xminusonetimesxminusonesquared.b, and then uses the two elementary facts

for every δ, ε > 0, f(x) ≤ δ implies x - 1 ≤ δ + δ^{1/2} ≤ (1+ε^{-1})δ + (1/4)ε

together with the optimization in ε performed afterwards.

Everything here is stated for real numbers only; no matrix, cube or coefficient data appears.

Main results

• invMulSubOneSq_le_add_sub_two: the two-sided pairing f(x) ≤ x + y - 2 whenever 1 ≤ x * y, which is how the printed operator inequalities are used at the level of quadratic forms;
• sub_one_le_add_sqrt_of_invMulSubOneSq_le: f(x) ≤ δ → x - 1 ≤ δ + δ^{1/2};
• sqrt_le_inv_mul_add_quarter: δ^{1/2} ≤ ε⁻¹ δ + ε/4;
• le_one_add_of_invMulSubOneSq_le: the combined ε-linearized bound f(x) ≤ δ → x ≤ 1 + (1 + ε⁻¹) δ + ε/4;
• le_add_sqrt_two_mul_of_forall_pos: the optimization in ε.

References

• ABK26.

noncomputable def Algsuperdiff.Section3.Provider.ErrorComparison.invMulSubOneSq (x : ℝ) : ℝ

The scalar function f(x) = x^{-1} (x-1)^2 of ABK26.

Equations

• Algsuperdiff.Section3.Provider.ErrorComparison.invMulSubOneSq x = x⁻¹ * (x - 1) ^ 2

theorem Algsuperdiff.Section3.Provider.ErrorComparison.invMulSubOneSq_eq_add_inv_sub_two {x : ℝ} (hx : 0 < x) : invMulSubOneSq x = x + x⁻¹ - 2

On the positive half-line, f(x) = x + x^{-1} - 2. This is the identity behind the printed algebraic identity closing e.xminusonetimesxminusonesquared.sstar.

theorem Algsuperdiff.Section3.Provider.ErrorComparison.invMulSubOneSq_le_add_sub_two {x y : ℝ} (hx : 0 < x) (hxy : 1 ≤ x * y) : invMulSubOneSq x ≤ x + y - 2

If x, y > 0 satisfy 1 ≤ x * y, then f(x) ≤ x + y - 2.

This is the scalar shadow of the printed operator inequalities: the quadratic forms of the two normalized coarse matrices always have product at least one, and their sum minus 2 therefore dominates f of either one.

theorem Algsuperdiff.Section3.Provider.ErrorComparison.sub_one_le_add_sqrt_of_invMulSubOneSq_le {x δ : ℝ} (hx : 0 < x) (hδ : 0 ≤ δ) (h : invMulSubOneSq x ≤ δ) : x - 1 ≤ δ + √δ

The printed implication "f(x) ≤ δ implies x - 1 ≤ δ + δ^{1/2}" (ABK26).

theorem Algsuperdiff.Section3.Provider.ErrorComparison.le_inv_mul_sq_add_quarter (r : ℝ) {ε : ℝ} (hε : 0 < ε) : r ≤ ε⁻¹ * r ^ 2 + ε / 4

The elementary Young inequality r ≤ ε^{-1} r² + (1/4) ε.

theorem Algsuperdiff.Section3.Provider.ErrorComparison.sqrt_le_inv_mul_add_quarter {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 < ε) : √δ ≤ ε⁻¹ * δ + ε / 4

The printed inequality δ^{1/2} ≤ ε^{-1} δ + (1/4) ε (ABK26).

theorem Algsuperdiff.Section3.Provider.ErrorComparison.le_one_add_of_invMulSubOneSq_le {x δ ε : ℝ} (hx : 0 < x) (hδ : 0 ≤ δ) (hε : 0 < ε) (h : invMulSubOneSq x ≤ δ) : x ≤ 1 + (1 + ε⁻¹) * δ + ε / 4

The ε-linearized form of the printed implication: f(x) ≤ δ implies x ≤ 1 + (1 + ε^{-1}) δ + (1/4) ε.

theorem Algsuperdiff.Section3.Provider.ErrorComparison.le_add_sqrt_two_mul_of_forall_pos {x K A : ℝ} (hA : 0 ≤ A) (h : ∀ (ε : ℝ), 0 < ε → x ≤ K + 2 * ε⁻¹ * A ^ 2 + ε / 4) : x ≤ K + √2 * A

The optimization in ε performed on ABK26: if x ≤ K + 2 ε^{-1} A² + (1/4) ε for every ε > 0, then x ≤ K + 2^{1/2} A.