Coarse-graining support: Support.Book.Ch05.Theorems.Section54.OneStepContraction.RealAlgebra

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Real algebra for the one-step contraction

The final proof chooses epsilon = delta^(1/4). This file isolates the elementary estimates for that choice.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepContractionEpsilon_pos {delta : ℝ} (hdelta_pos : 0 < delta) : 0 < oneStepContractionEpsilon delta

The one-step epsilon is positive for positive delta.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepContractionEpsilon_nonneg {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) : 0 ≤ oneStepContractionEpsilon delta

The one-step epsilon is nonnegative for nonnegative delta.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepContractionEpsilon_le_one {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) : oneStepContractionEpsilon delta ≤ 1

In the manuscript range, the one-step epsilon is at most one.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.delta_le_sqrt_of_pos_of_le_half {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) : delta ≤ √delta

The square root dominates delta on the manuscript range.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.sqrt_le_oneStepContractionEpsilon {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) : √delta ≤ oneStepContractionEpsilon delta

The quarter power dominates the square root when 0 < delta <= 1.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.delta_le_oneStepContractionEpsilon {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) : delta ≤ oneStepContractionEpsilon delta

The quarter power dominates delta on the manuscript range.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepContractionEpsilon_inv_mul_sqrt_eq {delta : ℝ} (hdelta_pos : 0 < delta) : (oneStepContractionEpsilon delta)⁻¹ * √delta = oneStepContractionEpsilon delta

With epsilon = delta^(1/4), the product epsilon^{-1} sqrt(delta) is again epsilon.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepContractionEpsilon_add_inv_mul_sqrt_le {delta : ℝ} (hdelta_pos : 0 < delta) : oneStepContractionEpsilon delta + (oneStepContractionEpsilon delta)⁻¹ * √delta ≤ 2 * oneStepContractionEpsilon delta

The final epsilon absorption used after the Section 5.3 estimate.